Theorem lmodsubdi

Description: Scalar multiplication distributive law for subtraction. ( hvsubdistr1 analogue, with longer proof since our scalar multiplication is not commutative.) (Contributed by NM, 2-Jul-2014)

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

Proof

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