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	54	grpmndd	$⊢ W \in LMod \to W \in Mnd$
56	55	ad2antll	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to W \in Mnd$
57		simpl	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to y \in ℕ_{0}$
58	32	adantl	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to X \in V$
59		eqid	$⊢ +_{W} = +_{W}$
60	1 5 59	mulgnn0p1	$⊢ (W \in Mnd \land y \in ℕ_{0} \land X \in V) \to (y + 1) \underset{˙}{\times} X = (y \underset{˙}{\times} X) +_{W} X$
61	56 57 58 60	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$
62	61	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)$
63		simpr	$⊢ ((R \in K \land X \in V) \land W \in LMod) \to W \in LMod$
64	63	adantl	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to W \in LMod$
65		simprll	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to R \in K$
66	1 5	mulgnn0cl	$⊢ (W \in Mnd \land y \in ℕ_{0} \land X \in V) \to y \underset{˙}{\times} X \in V$
67	56 57 58 66	syl3anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to y \underset{˙}{\times} X \in V$
68	1 59 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)$
69	64 65 67 58 68	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)$
70	62 69	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)$
71		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)$
72	70 71	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)$
73	2	lmodfgrp	$⊢ W \in LMod \to F \in Grp$
74	73	grpmndd	$⊢ W \in LMod \to F \in Mnd$
75	74	ad2antll	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to F \in Mnd$
76	4 6	mulgnn0cl	$⊢ (F \in Mnd \land y \in ℕ_{0} \land R \in K) \to y E R \in K$
77	75 57 65 76	syl3anc	$⊢ (y \in ℕ_{0} \land ((R \in K \land X \in V) \land W \in LMod)) \to y E R \in K$
78		eqid	$⊢ +_{F} = +_{F}$
79	1 59 2 3 4 78	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)$
80	64 77 65 58 79	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)$
81	4 6 78	mulgnn0p1	$⊢ (F \in Mnd \land y \in ℕ_{0} \land R \in K) \to (y + 1) E R = (y E R) +_{F} R$
82	75 57 65 81	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$
83	82	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$
84	83	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$
85	80 84	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$
86	85	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$
87	72 86	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$
88	87	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))$
89	88	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))$
90	12 18 24 30 53 89	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)$
91	90	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)))$
92	91	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)))$
93	92	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)$
94	93	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