lmodvsmmulgdi

Description: Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019)

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

Proof

Step	Hyp	Ref	Expression
1		lmodvsmmulgdi.v	$⊢ V = {Base}_{W}$
2		lmodvsmmulgdi.f	$⊢ F = Scalar (W)$
3		lmodvsmmulgdi.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodvsmmulgdi.k	$⊢ K = {Base}_{F}$
5		lmodvsmmulgdi.p	$⊢ \underset{˙}{\times} = \cdot_{W}$
6		lmodvsmmulgdi.e	$⊢ E = \cdot_{F}$
7		oveq1	$⊢ x = 0 \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = 0 \underset{˙}{\times} (C \underset{˙}{\cdot} X)$
8		oveq1	$⊢ x = 0 \to x E C = 0 E C$
9	8	oveq1d	$⊢ x = 0 \to (x E C) \underset{˙}{\cdot} X = (0 E C) \underset{˙}{\cdot} X$
10	7 9	eqeq12d	$⊢ x = 0 \to (x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X \leftrightarrow 0 \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (0 E C) \underset{˙}{\cdot} X)$
11	10	imbi2d	$⊢ x = 0 \to ((((C \in K \land X \in V) \land W \in LMod) \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X) \leftrightarrow (((C \in K \land X \in V) \land W \in LMod) \to 0 \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (0 E C) \underset{˙}{\cdot} X))$
12		oveq1	$⊢ x = y \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = y \underset{˙}{\times} (C \underset{˙}{\cdot} X)$
13		oveq1	$⊢ x = y \to x E C = y E C$
14	13	oveq1d	$⊢ x = y \to (x E C) \underset{˙}{\cdot} X = (y E C) \underset{˙}{\cdot} X$
15	12 14	eqeq12d	$⊢ x = y \to (x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X \leftrightarrow y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X)$
16	15	imbi2d	$⊢ x = y \to ((((C \in K \land X \in V) \land W \in LMod) \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X) \leftrightarrow (((C \in K \land X \in V) \land W \in LMod) \to y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X))$
17		oveq1	$⊢ x = y + 1 \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X)$
18		oveq1	$⊢ x = y + 1 \to x E C = (y + 1) E C$
19	18	oveq1d	$⊢ x = y + 1 \to (x E C) \underset{˙}{\cdot} X = ((y + 1) E C) \underset{˙}{\cdot} X$
20	17 19	eqeq12d	$⊢ x = y + 1 \to (x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X \leftrightarrow (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = ((y + 1) E C) \underset{˙}{\cdot} X)$
21	20	imbi2d	$⊢ x = y + 1 \to ((((C \in K \land X \in V) \land W \in LMod) \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X) \leftrightarrow (((C \in K \land X \in V) \land W \in LMod) \to (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = ((y + 1) E C) \underset{˙}{\cdot} X))$
22		oveq1	$⊢ x = N \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = N \underset{˙}{\times} (C \underset{˙}{\cdot} X)$
23		oveq1	$⊢ x = N \to x E C = N E C$
24	23	oveq1d	$⊢ x = N \to (x E C) \underset{˙}{\cdot} X = (N E C) \underset{˙}{\cdot} X$
25	22 24	eqeq12d	$⊢ x = N \to (x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X \leftrightarrow N \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (N E C) \underset{˙}{\cdot} X)$
26	25	imbi2d	$⊢ x = N \to ((((C \in K \land X \in V) \land W \in LMod) \to x \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (x E C) \underset{˙}{\cdot} X) \leftrightarrow (((C \in K \land X \in V) \land W \in LMod) \to N \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (N E C) \underset{˙}{\cdot} X))$
27		simpr	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to W \in LMod$
28		simpr	$⊢ (C \in K \land X \in V) \to X \in V$
29	28	adantr	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to X \in V$
30		eqid	$⊢ 0_{F} = 0_{F}$
31		eqid	$⊢ 0_{W} = 0_{W}$
32	1 2 3 30 31	lmod0vs	$⊢ (W \in LMod \land X \in V) \to 0_{F} \underset{˙}{\cdot} X = 0_{W}$
33	27 29 32	syl2anc	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to 0_{F} \underset{˙}{\cdot} X = 0_{W}$
34		simpl	$⊢ (C \in K \land X \in V) \to C \in K$
35	34	adantr	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to C \in K$
36	4 30 6	mulg0	$⊢ C \in K \to 0 E C = 0_{F}$
37	35 36	syl	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to 0 E C = 0_{F}$
38	37	oveq1d	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to (0 E C) \underset{˙}{\cdot} X = 0_{F} \underset{˙}{\cdot} X$
39	1 2 3 4	lmodvscl	$⊢ (W \in LMod \land C \in K \land X \in V) \to C \underset{˙}{\cdot} X \in V$
40	27 35 29 39	syl3anc	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to C \underset{˙}{\cdot} X \in V$
41	1 31 5	mulg0	$⊢ C \underset{˙}{\cdot} X \in V \to 0 \underset{˙}{\times} (C \underset{˙}{\cdot} X) = 0_{W}$
42	40 41	syl	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to 0 \underset{˙}{\times} (C \underset{˙}{\cdot} X) = 0_{W}$
43	33 38 42	3eqtr4rd	$⊢ ((C \in K \land X \in V) \land W \in LMod) \to 0 \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (0 E C) \underset{˙}{\cdot} X$
44		lmodgrp	$⊢ W \in LMod \to W \in Grp$
45	44	grpmndd	$⊢ W \in LMod \to W \in Mnd$
46	45	ad2antll	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to W \in Mnd$
47		simpl	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to y \in ℕ_{0}$
48	40	adantl	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to C \underset{˙}{\cdot} X \in V$
49		eqid	$⊢ +_{W} = +_{W}$
50	1 5 49	mulgnn0p1	$⊢ (W \in Mnd \land y \in ℕ_{0} \land C \underset{˙}{\cdot} X \in V) \to (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y \underset{˙}{\times} (C \underset{˙}{\cdot} X)) +_{W} (C \underset{˙}{\cdot} X)$
51	46 47 48 50	syl3anc	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y \underset{˙}{\times} (C \underset{˙}{\cdot} X)) +_{W} (C \underset{˙}{\cdot} X)$
52	51	adantr	$⊢ ((y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \land y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X) \to (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y \underset{˙}{\times} (C \underset{˙}{\cdot} X)) +_{W} (C \underset{˙}{\cdot} X)$
53		oveq1	$⊢ y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X \to (y \underset{˙}{\times} (C \underset{˙}{\cdot} X)) +_{W} (C \underset{˙}{\cdot} X) = ((y E C) \underset{˙}{\cdot} X) +_{W} (C \underset{˙}{\cdot} X)$
54	27	adantl	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to W \in LMod$
55	2	lmodring	$⊢ W \in LMod \to F \in Ring$
56		ringmnd	$⊢ F \in Ring \to F \in Mnd$
57	55 56	syl	$⊢ W \in LMod \to F \in Mnd$
58	57	ad2antll	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to F \in Mnd$
59		simprll	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to C \in K$
60	4 6 58 47 59	mulgnn0cld	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to y E C \in K$
61	29	adantl	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to X \in V$
62		eqid	$⊢ +_{F} = +_{F}$
63	1 49 2 3 4 62	lmodvsdir	$⊢ (W \in LMod \land (y E C \in K \land C \in K \land X \in V)) \to ((y E C) +_{F} C) \underset{˙}{\cdot} X = ((y E C) \underset{˙}{\cdot} X) +_{W} (C \underset{˙}{\cdot} X)$
64	54 60 59 61 63	syl13anc	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to ((y E C) +_{F} C) \underset{˙}{\cdot} X = ((y E C) \underset{˙}{\cdot} X) +_{W} (C \underset{˙}{\cdot} X)$
65	4 6 62	mulgnn0p1	$⊢ (F \in Mnd \land y \in ℕ_{0} \land C \in K) \to (y + 1) E C = (y E C) +_{F} C$
66	58 47 59 65	syl3anc	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to (y + 1) E C = (y E C) +_{F} C$
67	66	eqcomd	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to (y E C) +_{F} C = (y + 1) E C$
68	67	oveq1d	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to ((y E C) +_{F} C) \underset{˙}{\cdot} X = ((y + 1) E C) \underset{˙}{\cdot} X$
69	64 68	eqtr3d	$⊢ (y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \to ((y E C) \underset{˙}{\cdot} X) +_{W} (C \underset{˙}{\cdot} X) = ((y + 1) E C) \underset{˙}{\cdot} X$
70	53 69	sylan9eqr	$⊢ ((y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \land y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X) \to (y \underset{˙}{\times} (C \underset{˙}{\cdot} X)) +_{W} (C \underset{˙}{\cdot} X) = ((y + 1) E C) \underset{˙}{\cdot} X$
71	52 70	eqtrd	$⊢ ((y \in ℕ_{0} \land ((C \in K \land X \in V) \land W \in LMod)) \land y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X) \to (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = ((y + 1) E C) \underset{˙}{\cdot} X$
72	71	exp31	$⊢ y \in ℕ_{0} \to (((C \in K \land X \in V) \land W \in LMod) \to (y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X \to (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = ((y + 1) E C) \underset{˙}{\cdot} X))$
73	72	a2d	$⊢ y \in ℕ_{0} \to ((((C \in K \land X \in V) \land W \in LMod) \to y \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (y E C) \underset{˙}{\cdot} X) \to (((C \in K \land X \in V) \land W \in LMod) \to (y + 1) \underset{˙}{\times} (C \underset{˙}{\cdot} X) = ((y + 1) E C) \underset{˙}{\cdot} X))$
74	11 16 21 26 43 73	nn0ind	$⊢ N \in ℕ_{0} \to (((C \in K \land X \in V) \land W \in LMod) \to N \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (N E C) \underset{˙}{\cdot} X)$
75	74	exp4c	$⊢ N \in ℕ_{0} \to (C \in K \to (X \in V \to (W \in LMod \to N \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (N E C) \underset{˙}{\cdot} X)))$
76	75	3imp21	$⊢ (C \in K \land N \in ℕ_{0} \land X \in V) \to (W \in LMod \to N \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (N E C) \underset{˙}{\cdot} X)$
77	76	impcom	$⊢ (W \in LMod \land (C \in K \land N \in ℕ_{0} \land X \in V)) \to N \underset{˙}{\times} (C \underset{˙}{\cdot} X) = (N E C) \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem lmodvsmmulgdi

Proof