Theorem lmodvsinv2

Description: Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	lmodvsinv2.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	lmodvsinv2.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lmodvsinv2.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lmodvsinv2.n	⊢ 𝑁 = ( invg ‘ 𝑊 )
	lmodvsinv2.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	lmodvsinv2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmodvsinv2.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lmodvsinv2.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		lmodvsinv2.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		lmodvsinv2.n	⊢ 𝑁 = ( invg ‘ 𝑊 )
5		lmodvsinv2.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑊 ∈ LMod )
7		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
8	6 7	syl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑊 ∈ Grp )
9		simp3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
10		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
11		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
12	1 10 11 4	grprinv	⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
13	8 9 12	syl2anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
14	13	oveq2d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( 𝑅 · ( 0g ‘ 𝑊 ) ) )
15		simp2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ 𝐾 )
16	1 4	grpinvcl	⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
17	8 9 16	syl2anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 )
18	1 10 2 3 5	lmodvsdi	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ) ) → ( 𝑅 · ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) )
19	6 15 9 17 18	syl13anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑁 ‘ 𝑋 ) ) ) = ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) )
20	2 3 5 11	lmodvs0	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) → ( 𝑅 · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
21	6 15 20	syl2anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
22	14 19 21	3eqtr3d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑊 ) )
23	1 2 3 5	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · 𝑋 ) ∈ 𝐵 )
24	1 2 3 5	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ ( 𝑁 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 )
25	6 15 17 24	syl3anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 )
26	1 10 11 4	grpinvid1	⊢ ( ( 𝑊 ∈ Grp ∧ ( 𝑅 · 𝑋 ) ∈ 𝐵 ∧ ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ∈ 𝐵 ) → ( ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ↔ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑊 ) ) )
27	8 23 25 26	syl3anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ↔ ( ( 𝑅 · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑊 ) ) )
28	22 27	mpbird	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) = ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) )
29	28	eqcomd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · ( 𝑁 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )