Theorem lmodsubdir

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr2 analog.) (Contributed by NM, 2-Jul-2014)

	Ref	Expression
Hypotheses	lmodsubdir.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lmodsubdir.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lmodsubdir.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lmodsubdir.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lmodsubdir.m	⊢ − = ( -g ‘ 𝑊 )
	lmodsubdir.s	⊢ 𝑆 = ( -g ‘ 𝐹 )
	lmodsubdir.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lmodsubdir.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	lmodsubdir.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
	lmodsubdir.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	lmodsubdir	⊢ ( 𝜑 → ( ( 𝐴 𝑆 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmodsubdir.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lmodsubdir.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		lmodsubdir.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		lmodsubdir.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
5		lmodsubdir.m	⊢ − = ( -g ‘ 𝑊 )
6		lmodsubdir.s	⊢ 𝑆 = ( -g ‘ 𝐹 )
7		lmodsubdir.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		lmodsubdir.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
9		lmodsubdir.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
10		lmodsubdir.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11	3	lmodring	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
12	7 11	syl	⊢ ( 𝜑 → 𝐹 ∈ Ring )
13		ringgrp	⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Grp )
14	12 13	syl	⊢ ( 𝜑 → 𝐹 ∈ Grp )
15		eqid	⊢ ( invg ‘ 𝐹 ) = ( invg ‘ 𝐹 )
16	4 15	grpinvcl	⊢ ( ( 𝐹 ∈ Grp ∧ 𝐵 ∈ 𝐾 ) → ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ∈ 𝐾 )
17	14 9 16	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ∈ 𝐾 )
18		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
19		eqid	⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
20	1 18 3 2 4 19	lmodvsdir	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∈ 𝐾 ∧ ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) ) )
21	7 8 17 10 20	syl13anc	⊢ ( 𝜑 → ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) ) )
22		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
23		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
24	4 22 23 15 12 9	ringnegl	⊢ ( 𝜑 → ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) = ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) )
25	24	oveq1d	⊢ ( 𝜑 → ( ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) )
26	4 23	ringidcl	⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
27	12 26	syl	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ 𝐾 )
28	4 15	grpinvcl	⊢ ( ( 𝐹 ∈ Grp ∧ ( 1r ‘ 𝐹 ) ∈ 𝐾 ) → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
29	14 27 28	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 )
30	1 3 2 4 22	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) )
31	7 29 9 10 30	syl13anc	⊢ ( 𝜑 → ( ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) ( .r ‘ 𝐹 ) 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) )
32	25 31	eqtr3d	⊢ ( 𝜑 → ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) = ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) )
33	32	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
34	21 33	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
35	4 19 15 6	grpsubval	⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 𝑆 𝐵 ) = ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) )
36	8 9 35	syl2anc	⊢ ( 𝜑 → ( 𝐴 𝑆 𝐵 ) = ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) )
37	36	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 𝑆 𝐵 ) · 𝑋 ) = ( ( 𝐴 ( +g ‘ 𝐹 ) ( ( invg ‘ 𝐹 ) ‘ 𝐵 ) ) · 𝑋 ) )
38	1 3 2 4	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
39	7 8 10 38	syl3anc	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
40	1 3 2 4	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
41	7 9 10 40	syl3anc	⊢ ( 𝜑 → ( 𝐵 · 𝑋 ) ∈ 𝑉 )
42	1 18 5 3 2 15 23	lmodvsubval2	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐵 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
43	7 39 41 42	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) = ( ( 𝐴 · 𝑋 ) ( +g ‘ 𝑊 ) ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · ( 𝐵 · 𝑋 ) ) ) )
44	34 37 43	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 𝑆 𝐵 ) · 𝑋 ) = ( ( 𝐴 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )