lmodvsmdi

Description: Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019)

	Ref	Expression
Hypotheses	lmodvsmdi.v	$⊢ V = {Base}_{W}$
	lmodvsmdi.f	$⊢ F = Scalar (W)$
	lmodvsmdi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lmodvsmdi.k	$⊢ K = {Base}_{F}$
	lmodvsmdi.p	$⊢ \underset{˙}{\times} = \cdot_{W}$
	lmodvsmdi.e	$⊢ E = \cdot_{F}$
Assertion	lmodvsmdi	$⊢ (W \in LMod \land (R \in K \land N \in ℕ_{0} \land X \in V)) \to R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		lmodvsmdi.v	$⊢ V = {Base}_{W}$
2		lmodvsmdi.f	$⊢ F = Scalar (W)$
3		lmodvsmdi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodvsmdi.k	$⊢ K = {Base}_{F}$
5		lmodvsmdi.p	$⊢ \underset{˙}{\times} = \cdot_{W}$
6		lmodvsmdi.e	$⊢ E = \cdot_{F}$
7		oveq1	$⊢ x = 0 \to x \underset{˙}{\times} X = 0 \underset{˙}{\times} X$
8	7	oveq2d	$⊢ x = 0 \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = R \underset{˙}{\cdot} (0 \underset{˙}{\times} X)$
9		oveq1	$⊢ x = 0 \to x E R = 0 E R$
10	9	oveq1d	$⊢ x = 0 \to (x E R) \underset{˙}{\cdot} X = (0 E R) \underset{˙}{\cdot} X$
11	8 10	eqeq12d	$⊢ x = 0 \to (R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X \leftrightarrow R \underset{˙}{\cdot} (0 \underset{˙}{\times} X) = (0 E R) \underset{˙}{\cdot} X)$
12	11	imbi2d	$⊢ x = 0 \to ((((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X) \leftrightarrow (((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (0 \underset{˙}{\times} X) = (0 E R) \underset{˙}{\cdot} X))$
13		oveq1	$⊢ x = y \to x \underset{˙}{\times} X = y \underset{˙}{\times} X$
14	13	oveq2d	$⊢ x = y \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = R \underset{˙}{\cdot} (y \underset{˙}{\times} X)$
15		oveq1	$⊢ x = y \to x E R = y E R$
16	15	oveq1d	$⊢ x = y \to (x E R) \underset{˙}{\cdot} X = (y E R) \underset{˙}{\cdot} X$
17	14 16	eqeq12d	$⊢ x = y \to (R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X \leftrightarrow R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X)$
18	17	imbi2d	$⊢ x = y \to ((((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X) \leftrightarrow (((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X))$
19		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\times} X = (y + 1) \underset{˙}{\times} X$
20	19	oveq2d	$⊢ x = y + 1 \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X)$
21		oveq1	$⊢ x = y + 1 \to x E R = (y + 1) E R$
22	21	oveq1d	$⊢ x = y + 1 \to (x E R) \underset{˙}{\cdot} X = ((y + 1) E R) \underset{˙}{\cdot} X$
23	20 22	eqeq12d	$⊢ x = y + 1 \to (R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X \leftrightarrow R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = ((y + 1) E R) \underset{˙}{\cdot} X)$
24	23	imbi2d	$⊢ x = y + 1 \to ((((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X) \leftrightarrow (((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = ((y + 1) E R) \underset{˙}{\cdot} X))$
25		oveq1	$⊢ x = N \to x \underset{˙}{\times} X = N \underset{˙}{\times} X$
26	25	oveq2d	$⊢ x = N \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = R \underset{˙}{\cdot} (N \underset{˙}{\times} X)$
27		oveq1	$⊢ x = N \to x E R = N E R$
28	27	oveq1d	$⊢ x = N \to (x E R) \underset{˙}{\cdot} X = (N E R) \underset{˙}{\cdot} X$
29	26 28	eqeq12d	$⊢ x = N \to (R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X \leftrightarrow R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X)$
30	29	imbi2d	$⊢ x = N \to ((((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (x \underset{˙}{\times} X) = (x E R) \underset{˙}{\cdot} X) \leftrightarrow (((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X))$
31		simpr	$⊢ (R \in K \land X \in V) \to X \in V$
32	31	adantr	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to X \in V$
33		eqid	$⊢ 0_{W} = 0_{W}$
34	1 33 5	mulg0	$⊢ X \in V \to 0 \underset{˙}{\times} X = 0_{W}$
35	32 34	syl	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to 0 \underset{˙}{\times} X = 0_{W}$
36	35	oveq2d	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (0 \underset{˙}{\times} X) = R \underset{˙}{\cdot} 0_{W}$
37		simpl	$⊢ (R \in K \land X \in V) \to R \in K$
38	37	anim1i	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to (R \in K \land W \in LMod)$
39	38	ancomd	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to (W \in LMod \land R \in K)$
40	2 3 4 33	lmodvs0	$⊢ (W \in LMod \land R \in K) \to R \underset{˙}{\cdot} 0_{W} = 0_{W}$
41	39 40	syl	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} 0_{W} = 0_{W}$
42	31	anim1i	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to (X \in V \land W \in LMod)$
43	42	ancomd	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to (W \in LMod \land X \in V)$
44		eqid	$⊢ 0_{F} = 0_{F}$
45	1 2 3 44 33	lmod0vs	$⊢ (W \in LMod \land X \in V) \to 0_{F} \underset{˙}{\cdot} X = 0_{W}$
46	43 45	syl	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to 0_{F} \underset{˙}{\cdot} X = 0_{W}$
47	37	adantr	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to R \in K$
48	4 44 6	mulg0	$⊢ R \in K \to 0 E R = 0_{F}$
49	48	eqcomd	$⊢ R \in K \to 0_{F} = 0 E R$
50	47 49	syl	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to 0_{F} = 0 E R$
51	50	oveq1d	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to 0_{F} \underset{˙}{\cdot} X = (0 E R) \underset{˙}{\cdot} X$
52	41 46 51	3eqtr2d	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} 0_{W} = (0 E R) \underset{˙}{\cdot} X$
53	36 52	eqtrd	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (0 \underset{˙}{\times} X) = (0 E R) \underset{˙}{\cdot} X$
54		lmodgrp	$⊢ W \in LMod \to W \in Grp$
55		grpmnd	$⊢ W \in Grp \to W \in Mnd$
56	54 55	syl	$⊢ W \in LMod \to W \in Mnd$
57	56	ad2antll	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to W \in Mnd$
58		simpl	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to y \in ℕ_{0}$
59	32	adantl	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to X \in V$
60		eqid	$⊢ +_{W} = +_{W}$
61	1 5 60	mulgnn0p1	$⊢ (W \in Mnd \land y \in ℕ_{0} \land X \in V) \to (y + 1) \underset{˙}{\times} X = (y \underset{˙}{\times} X) +_{W} X$
62	57 58 59 61	syl3anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to (y + 1) \underset{˙}{\times} X = (y \underset{˙}{\times} X) +_{W} X$
63	62	oveq2d	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = R \underset{˙}{\cdot} ((y \underset{˙}{\times} X) +_{W} X)$
64		simpr	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to W \in LMod$
65	64	adantl	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to W \in LMod$
66		simprll	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to R \in K$
67	1 5	mulgnn0cl	$⊢ (W \in Mnd \land y \in ℕ_{0} \land X \in V) \to y \underset{˙}{\times} X \in V$
68	57 58 59 67	syl3anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to y \underset{˙}{\times} X \in V$
69	1 60 2 3 4	lmodvsdi	$⊢ (W \in LMod \land (R \in K \land y \underset{˙}{\times} X \in V \land X \in V)) \to R \underset{˙}{\cdot} ((y \underset{˙}{\times} X) +_{W} X) = (R \underset{˙}{\cdot} (y \underset{˙}{\times} X)) +_{W} (R \underset{˙}{\cdot} X)$
70	65 66 68 59 69	syl13anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to R \underset{˙}{\cdot} ((y \underset{˙}{\times} X) +_{W} X) = (R \underset{˙}{\cdot} (y \underset{˙}{\times} X)) +_{W} (R \underset{˙}{\cdot} X)$
71	63 70	eqtrd	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = (R \underset{˙}{\cdot} (y \underset{˙}{\times} X)) +_{W} (R \underset{˙}{\cdot} X)$
72		oveq1	$⊢ R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X \to (R \underset{˙}{\cdot} (y \underset{˙}{\times} X)) +_{W} (R \underset{˙}{\cdot} X) = ((y E R) \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X)$
73	71 72	sylan9eq	$⊢ ((y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \land R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X) \to R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = ((y E R) \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X)$
74	2	lmodfgrp	$⊢ W \in LMod \to F \in Grp$
75		grpmnd	$⊢ F \in Grp \to F \in Mnd$
76	74 75	syl	$⊢ W \in LMod \to F \in Mnd$
77	76	ad2antll	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to F \in Mnd$
78	4 6	mulgnn0cl	$⊢ (F \in Mnd \land y \in ℕ_{0} \land R \in K) \to y E R \in K$
79	77 58 66 78	syl3anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to y E R \in K$
80		eqid	$⊢ +_{F} = +_{F}$
81	1 60 2 3 4 80	lmodvsdir	$⊢ (W \in LMod \land (y E R \in K \land R \in K \land X \in V)) \to ((y E R) +_{F} R) \underset{˙}{\cdot} X = ((y E R) \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X)$
82	65 79 66 59 81	syl13anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to ((y E R) +_{F} R) \underset{˙}{\cdot} X = ((y E R) \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X)$
83	4 6 80	mulgnn0p1	$⊢ (F \in Mnd \land y \in ℕ_{0} \land R \in K) \to (y + 1) E R = (y E R) +_{F} R$
84	77 58 66 83	syl3anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to (y + 1) E R = (y E R) +_{F} R$
85	84	eqcomd	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to (y E R) +_{F} R = (y + 1) E R$
86	85	oveq1d	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to ((y E R) +_{F} R) \underset{˙}{\cdot} X = ((y + 1) E R) \underset{˙}{\cdot} X$
87	82 86	eqtr3d	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to ((y E R) \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X) = ((y + 1) E R) \underset{˙}{\cdot} X$
88	87	adantr	$⊢ ((y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \land R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X) \to ((y E R) \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X) = ((y + 1) E R) \underset{˙}{\cdot} X$
89	73 88	eqtrd	$⊢ ((y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \land R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X) \to R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = ((y + 1) E R) \underset{˙}{\cdot} X$
90	89	exp31	$⊢ y \in ℕ_{0} \to (((R \in K \land X \in V) \land W \in LMod) \to (R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X \to R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = ((y + 1) E R) \underset{˙}{\cdot} X))$
91	90	a2d	$⊢ y \in ℕ_{0} \to ((((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (y \underset{˙}{\times} X) = (y E R) \underset{˙}{\cdot} X) \to (((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} ((y + 1) \underset{˙}{\times} X) = ((y + 1) E R) \underset{˙}{\cdot} X))$
92	12 18 24 30 53 91	nn0ind	$⊢ N \in ℕ_{0} \to (((R \in K \land X \in V) \land W \in LMod) \to R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X)$
93	92	exp4c	$⊢ N \in ℕ_{0} \to (R \in K \to (X \in V \to (W \in LMod \to R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X)))$
94	93	com12	$⊢ R \in K \to (N \in ℕ_{0} \to (X \in V \to (W \in LMod \to R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X)))$
95	94	3imp	$⊢ (R \in K \land N \in ℕ_{0} \land X \in V) \to (W \in LMod \to R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X)$
96	95	impcom	$⊢ (W \in LMod \land (R \in K \land N \in ℕ_{0} \land X \in V)) \to R \underset{˙}{\cdot} (N \underset{˙}{\times} X) = (N E R) \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem lmodvsmdi

Proof