Metamath Proof Explorer

Theorem lvecvscan

Description: Cancellation law for scalar multiplication. ( hvmulcan analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lvecmulcan.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lvecmulcan.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lvecmulcan.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lvecmulcan.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lvecmulcan.o ⊢ 0 = ( 0g ‘ 𝐹 )
lvecmulcan.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lvecmulcan.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
lvecmulcan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lvecmulcan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lvecmulcan.n ⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion lvecvscan ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝐴 · 𝑌 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 lvecmulcan.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lvecmulcan.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lvecmulcan.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lvecmulcan.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lvecmulcan.o ⊢ 0 = ( 0g ‘ 𝐹 )
6 lvecmulcan.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lvecmulcan.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
8 lvecmulcan.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9 lvecmulcan.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10 lvecmulcan.n ⊢ ( 𝜑 → 𝐴 ≠ 0 )
11 df-ne ⊢ ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
12 biorf ⊢ ( ¬ 𝐴 = 0 → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ↔ ( 𝐴 = 0 ∨ ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ) ) )
13 11 12 sylbi ⊢ ( 𝐴 ≠ 0 → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ↔ ( 𝐴 = 0 ∨ ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ) ) )
14 10 13 syl ⊢ ( 𝜑 → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ↔ ( 𝐴 = 0 ∨ ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ) ) )
15 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
16 6 15 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
17 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
18 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
19 1 17 18 lmodsubeq0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ↔ 𝑋 = 𝑌 ) )
20 16 8 9 19 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ↔ 𝑋 = 𝑌 ) )
21 1 2 3 4 18 16 7 8 9 lmodsubdi ⊢ ( 𝜑 → ( 𝐴 · ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) ) = ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐴 · 𝑌 ) ) )
22 21 eqeq1d ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) ) = ( 0g ‘ 𝑊 ) ↔ ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐴 · 𝑌 ) ) = ( 0g ‘ 𝑊 ) ) )
23 1 18 lmodvsubcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
24 16 8 9 23 syl3anc ⊢ ( 𝜑 → ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
25 1 2 3 4 5 17 6 7 24 lvecvs0or ⊢ ( 𝜑 → ( ( 𝐴 · ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) ) = ( 0g ‘ 𝑊 ) ↔ ( 𝐴 = 0 ∨ ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ) ) )
26 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
27 16 7 8 26 syl3anc ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
28 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐴 · 𝑌 ) ∈ 𝑉 )
29 16 7 9 28 syl3anc ⊢ ( 𝜑 → ( 𝐴 · 𝑌 ) ∈ 𝑉 )
30 1 17 18 lmodsubeq0 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐴 · 𝑌 ) ∈ 𝑉 ) → ( ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐴 · 𝑌 ) ) = ( 0g ‘ 𝑊 ) ↔ ( 𝐴 · 𝑋 ) = ( 𝐴 · 𝑌 ) ) )
31 16 27 29 30 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐴 · 𝑌 ) ) = ( 0g ‘ 𝑊 ) ↔ ( 𝐴 · 𝑋 ) = ( 𝐴 · 𝑌 ) ) )
32 22 25 31 3bitr3d ⊢ ( 𝜑 → ( ( 𝐴 = 0 ∨ ( 𝑋 ( -g ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) ) ↔ ( 𝐴 · 𝑋 ) = ( 𝐴 · 𝑌 ) ) )
33 14 20 32 3bitr3rd ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝐴 · 𝑌 ) ↔ 𝑋 = 𝑌 ) )