R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0) ↔ ∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
⊢ IsOrthoᵢ B v ↔ IsOrthoᵢ (flip B) v
simp_rw [isOrthoᵢ_def]
case mp
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑(flip B) (v i)) (v j) = 0

case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v i)) (v j) = 0
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0) ↔ ∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0
constructor <;> intro h i j hij
case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v j)) (v i) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v i)) (v j) = 0
case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑(flip B) (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v i)) (v j) = 0
simp_rw [flip_apply] at h
no goals
case mpr
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v j)) (v i) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v i)) (v j) = 0
exact h j i (Ne.symm hij)
case mp
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v j)) (v i) = 0
case mp
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑(flip B) (v i)) (v j) = 0
rw [flip_apply]
no goals
case mp
R : Type u_2
R₁ : Type u_1
R₂ : Type ?u.29360
R₃ : Type ?u.29363
M : Type ?u.29366
M₁ : Type u_3
M₂ : Type ?u.29372
Mₗ₁ : Type ?u.29375
Mₗ₁' : Type ?u.29378
Mₗ₂ : Type ?u.29381
Mₗ₂' : Type ?u.29384
K : Type ?u.29387
K₁ : Type ?u.29390
K₂ : Type ?u.29393
V : Type ?u.29396
V₁ : Type ?u.29399
V₂ : Type ?u.29402
n : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] R
v : n → M₁
h : ∀ (i j : n), i ≠ j → ↑(↑B (v i)) (v j) = 0
i j : n
hij : i ≠ j
⊢ ↑(↑B (v j)) (v i) = 0
exact h j i (Ne.symm hij)