Theorem lmodvsinv

Description: Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lmodvsinv.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lmodvsinv.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		lmodvsinv.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		lmodvsinv.n	⊢ 𝑁 = ( invg ‘ 𝑊 )
5		lmodvsinv.m	⊢ 𝑀 = ( invg ‘ 𝐹 )
6		lmodvsinv.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
7		simp1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑊 ∈ LMod )
8	2	lmodring	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
9	8	3ad2ant1	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝐹 ∈ Ring )
10		ringgrp	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
11	9 10	syl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝐹 ∈ Grp )
12		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
13	6 12	ringidcl	⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
14	9 13	syl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
15	6 5	grpinvcl	⊢ ( ( 𝐹 ∈ Grp ∧ ( 1r ‘ 𝐹 ) ∈ 𝐾 ) → ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
16	11 14 15	syl2anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
17		simp2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑅 ∈ 𝐾 )
18		simp3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
19		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
20	1 2 3 6 19	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝑅 · 𝑋 ) ) )
21	7 16 17 18 20	syl13anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝑅 · 𝑋 ) ) )
22	6 19 12 5 9 17	ringnegl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝑅 ) = ( 𝑀 ‘ 𝑅 ) )
23	22	oveq1d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( 𝑀 ‘ 𝑅 ) · 𝑋 ) )
24	1 2 3 6	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 · 𝑋 ) ∈ 𝐵 )
25	1 4 2 3 12 5	lmodvneg1	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝑅 · 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )
26	7 24 25	syl2anc	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ ( 1r ‘ 𝐹 ) ) · ( 𝑅 · 𝑋 ) ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )
27	21 23 26	3eqtr3d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 ‘ 𝑅 ) · 𝑋 ) = ( 𝑁 ‘ ( 𝑅 · 𝑋 ) ) )