Metamath Proof Explorer

Theorem lvecvscan2

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

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

Proof

Step Hyp Ref Expression
1 lvecmulcan2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lvecmulcan2.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lvecmulcan2.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lvecmulcan2.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lvecmulcan2.o ⊢ 0 = ( 0g ‘ 𝑊 )
6 lvecmulcan2.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lvecmulcan2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
8 lvecmulcan2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
9 lvecmulcan2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lvecmulcan2.n ⊢ ( 𝜑 → 𝑋 ≠ 0 )
11 10 neneqd ⊢ ( 𝜑 → ¬ 𝑋 = 0 )
12 biorf ⊢ ( ¬ 𝑋 = 0 → ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ↔ ( 𝑋 = 0 ∨ ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ) ) )
13 orcom ⊢ ( ( 𝑋 = 0 ∨ ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ) ↔ ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ∨ 𝑋 = 0 ) )
14 12 13 bitrdi ⊢ ( ¬ 𝑋 = 0 → ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ↔ ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ∨ 𝑋 = 0 ) ) )
15 11 14 syl ⊢ ( 𝜑 → ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ↔ ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ∨ 𝑋 = 0 ) ) )
16 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
17 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
18 6 17 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
19 3 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
20 18 19 syl ⊢ ( 𝜑 → 𝐹 ∈ Grp )
21 eqid ⊢ ( -g ‘ 𝐹 ) = ( -g ‘ 𝐹 )
22 4 21 grpsubcl ⊢ ( ( 𝐹 ∈ Grp ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) ∈ 𝐾 )
23 20 7 8 22 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) ∈ 𝐾 )
24 1 2 3 4 16 5 6 23 9 lvecvs0or ⊢ ( 𝜑 → ( ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = 0 ↔ ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ∨ 𝑋 = 0 ) ) )
25 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
26 1 2 3 4 25 21 18 7 8 9 lmodsubdir ⊢ ( 𝜑 → ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝑋 ) ) )
27 26 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = 0 ↔ ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝑋 ) ) = 0 ) )
28 15 24 27 3bitr2rd ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝑋 ) ) = 0 ↔ ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ) )
29 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
30 18 7 9 29 syl3anc ⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
31 1 3 2 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
32 18 8 9 31 syl3anc ⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
33 1 5 25 lmodsubeq0 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐵 · 𝑋 ) ∈ 𝑉 ) → ( ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝑋 ) ) = 0 ↔ ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑋 ) ) )
34 18 30 32 33 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐴 · 𝑋 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝑋 ) ) = 0 ↔ ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑋 ) ) )
35 4 16 21 grpsubeq0 ⊢ ( ( 𝐹 ∈ Grp ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ↔ 𝐴 = 𝐵 ) )
36 20 7 8 35 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 0g ‘ 𝐹 ) ↔ 𝐴 = 𝐵 ) )
37 28 34 36 3bitr3d ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑋 ) ↔ 𝐴 = 𝐵 ) )