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	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = ( 𝐵 · 𝑋 ) ↔ 𝐴 = 𝐵 ) )