prdslmodd

Description: The product of a family of left modules is a left module. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdslmodd.y	$⊢ Y = S ⨉_{𝑠} R$
	prdslmodd.s	$⊢ φ \to S \in Ring$
	prdslmodd.i	$⊢ φ \to I \in V$
	prdslmodd.rm	$⊢ φ \to R : I ⟶ LMod$
	prdslmodd.rs	$⊢ (φ \land y \in I) \to Scalar (R (y)) = S$
Assertion	prdslmodd	$⊢ φ \to Y \in LMod$

Proof

Step	Hyp	Ref	Expression
1		prdslmodd.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdslmodd.s	$⊢ φ \to S \in Ring$
3		prdslmodd.i	$⊢ φ \to I \in V$
4		prdslmodd.rm	$⊢ φ \to R : I ⟶ LMod$
5		prdslmodd.rs	$⊢ (φ \land y \in I) \to Scalar (R (y)) = S$
6		eqidd	$⊢ φ \to {Base}_{Y} = {Base}_{Y}$
7		eqidd	$⊢ φ \to +_{Y} = +_{Y}$
8	4 3	fexd	$⊢ φ \to R \in V$
9	1 2 8	prdssca	$⊢ φ \to S = Scalar (Y)$
10		eqidd	$⊢ φ \to \cdot_{Y} = \cdot_{Y}$
11		eqidd	$⊢ φ \to {Base}_{S} = {Base}_{S}$
12		eqidd	$⊢ φ \to +_{S} = +_{S}$
13		eqidd	$⊢ φ \to \cdot_{S} = \cdot_{S}$
14		eqidd	$⊢ φ \to 1_{S} = 1_{S}$
15		lmodgrp	$⊢ a \in LMod \to a \in Grp$
16	15	ssriv	$⊢ LMod \subseteq Grp$
17		fss	$⊢ (R : I ⟶ LMod \land LMod \subseteq Grp) \to R : I ⟶ Grp$
18	4 16 17	sylancl	$⊢ φ \to R : I ⟶ Grp$
19	1 3 2 18	prdsgrpd	$⊢ φ \to Y \in Grp$
20		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
21		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
22		eqid	$⊢ {Base}_{S} = {Base}_{S}$
23	2	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y})) \to S \in Ring$
24	3	elexd	$⊢ φ \to I \in V$
25	24	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y})) \to I \in V$
26	4	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y})) \to R : I ⟶ LMod$
27		simprl	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y})) \to a \in {Base}_{S}$
28		simprr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y})) \to b \in {Base}_{Y}$
29	5	adantlr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y})) \land y \in I) \to Scalar (R (y)) = S$
30	1 20 21 22 23 25 26 27 28 29	prdsvscacl	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y})) \to a \cdot_{Y} b \in {Base}_{Y}$
31	30	3impb	$⊢ (φ \land a \in {Base}_{S} \land b \in {Base}_{Y}) \to a \cdot_{Y} b \in {Base}_{Y}$
32	4	ffvelrnda	$⊢ (φ \land y \in I) \to R (y) \in LMod$
33	32	adantlr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to R (y) \in LMod$
34		simplr1	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a \in {Base}_{S}$
35	5	fveq2d	$⊢ (φ \land y \in I) \to {Base}_{Scalar (R (y))} = {Base}_{S}$
36	35	adantlr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to {Base}_{Scalar (R (y))} = {Base}_{S}$
37	34 36	eleqtrrd	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a \in {Base}_{Scalar (R (y))}$
38	2	ad2antrr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to S \in Ring$
39	24	ad2antrr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to I \in V$
40	4	ffnd	$⊢ φ \to R Fn I$
41	40	ad2antrr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to R Fn I$
42		simplr2	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to b \in {Base}_{Y}$
43		simpr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to y \in I$
44	1 20 38 39 41 42 43	prdsbasprj	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to b (y) \in {Base}_{R (y)}$
45		simplr3	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to c \in {Base}_{Y}$
46	1 20 38 39 41 45 43	prdsbasprj	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to c (y) \in {Base}_{R (y)}$
47		eqid	$⊢ {Base}_{R (y)} = {Base}_{R (y)}$
48		eqid	$⊢ +_{R (y)} = +_{R (y)}$
49		eqid	$⊢ Scalar (R (y)) = Scalar (R (y))$
50		eqid	$⊢ \cdot_{R (y)} = \cdot_{R (y)}$
51		eqid	$⊢ {Base}_{Scalar (R (y))} = {Base}_{Scalar (R (y))}$
52	47 48 49 50 51	lmodvsdi	$⊢ (R (y) \in LMod \land (a \in {Base}_{Scalar (R (y))} \land b (y) \in {Base}_{R (y)} \land c (y) \in {Base}_{R (y)})) \to a \cdot_{R (y)} (b (y) +_{R (y)} c (y)) = (a \cdot_{R (y)} b (y)) +_{R (y)} (a \cdot_{R (y)} c (y))$
53	33 37 44 46 52	syl13anc	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a \cdot_{R (y)} (b (y) +_{R (y)} c (y)) = (a \cdot_{R (y)} b (y)) +_{R (y)} (a \cdot_{R (y)} c (y))$
54		eqid	$⊢ +_{Y} = +_{Y}$
55	1 20 38 39 41 42 45 54 43	prdsplusgfval	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (b +_{Y} c) (y) = b (y) +_{R (y)} c (y)$
56	55	oveq2d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a \cdot_{R (y)} (b +_{Y} c) (y) = a \cdot_{R (y)} (b (y) +_{R (y)} c (y))$
57	1 20 21 22 38 39 41 34 42 43	prdsvscafval	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{Y} b) (y) = a \cdot_{R (y)} b (y)$
58	1 20 21 22 38 39 41 34 45 43	prdsvscafval	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{Y} c) (y) = a \cdot_{R (y)} c (y)$
59	57 58	oveq12d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{Y} b) (y) +_{R (y)} (a \cdot_{Y} c) (y) = (a \cdot_{R (y)} b (y)) +_{R (y)} (a \cdot_{R (y)} c (y))$
60	53 56 59	3eqtr4d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \land y \in I) \to a \cdot_{R (y)} (b +_{Y} c) (y) = (a \cdot_{Y} b) (y) +_{R (y)} (a \cdot_{Y} c) (y)$
61	60	mpteq2dva	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to (y \in I ⟼ a \cdot_{R (y)} (b +_{Y} c) (y)) = (y \in I ⟼ (a \cdot_{Y} b) (y) +_{R (y)} (a \cdot_{Y} c) (y))$
62	2	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to S \in Ring$
63	24	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to I \in V$
64	40	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to R Fn I$
65		simpr1	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a \in {Base}_{S}$
66	19	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to Y \in Grp$
67		simpr2	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to b \in {Base}_{Y}$
68		simpr3	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to c \in {Base}_{Y}$
69	20 54	grpcl	$⊢ (Y \in Grp \land b \in {Base}_{Y} \land c \in {Base}_{Y}) \to b +_{Y} c \in {Base}_{Y}$
70	66 67 68 69	syl3anc	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to b +_{Y} c \in {Base}_{Y}$
71	1 20 21 22 62 63 64 65 70	prdsvscaval	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a \cdot_{Y} (b +_{Y} c) = (y \in I ⟼ a \cdot_{R (y)} (b +_{Y} c) (y))$
72	30	3adantr3	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a \cdot_{Y} b \in {Base}_{Y}$
73	2	adantr	$⊢ (φ \land (a \in {Base}_{S} \land c \in {Base}_{Y})) \to S \in Ring$
74	24	adantr	$⊢ (φ \land (a \in {Base}_{S} \land c \in {Base}_{Y})) \to I \in V$
75	4	adantr	$⊢ (φ \land (a \in {Base}_{S} \land c \in {Base}_{Y})) \to R : I ⟶ LMod$
76		simprl	$⊢ (φ \land (a \in {Base}_{S} \land c \in {Base}_{Y})) \to a \in {Base}_{S}$
77		simprr	$⊢ (φ \land (a \in {Base}_{S} \land c \in {Base}_{Y})) \to c \in {Base}_{Y}$
78	5	adantlr	$⊢ ((φ \land (a \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to Scalar (R (y)) = S$
79	1 20 21 22 73 74 75 76 77 78	prdsvscacl	$⊢ (φ \land (a \in {Base}_{S} \land c \in {Base}_{Y})) \to a \cdot_{Y} c \in {Base}_{Y}$
80	79	3adantr2	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a \cdot_{Y} c \in {Base}_{Y}$
81	1 20 62 63 64 72 80 54	prdsplusgval	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to (a \cdot_{Y} b) +_{Y} (a \cdot_{Y} c) = (y \in I ⟼ (a \cdot_{Y} b) (y) +_{R (y)} (a \cdot_{Y} c) (y))$
82	61 71 81	3eqtr4d	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{Y} \land c \in {Base}_{Y})) \to a \cdot_{Y} (b +_{Y} c) = (a \cdot_{Y} b) +_{Y} (a \cdot_{Y} c)$
83	2	ad2antrr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to S \in Ring$
84	24	ad2antrr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to I \in V$
85	40	ad2antrr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to R Fn I$
86		simplr1	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to a \in {Base}_{S}$
87		simplr3	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to c \in {Base}_{Y}$
88		simpr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to y \in I$
89	1 20 21 22 83 84 85 86 87 88	prdsvscafval	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{Y} c) (y) = a \cdot_{R (y)} c (y)$
90		simplr2	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to b \in {Base}_{S}$
91	1 20 21 22 83 84 85 90 87 88	prdsvscafval	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (b \cdot_{Y} c) (y) = b \cdot_{R (y)} c (y)$
92	89 91	oveq12d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{Y} c) (y) +_{R (y)} (b \cdot_{Y} c) (y) = (a \cdot_{R (y)} c (y)) +_{R (y)} (b \cdot_{R (y)} c (y))$
93	32	adantlr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to R (y) \in LMod$
94	35	adantlr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to {Base}_{Scalar (R (y))} = {Base}_{S}$
95	86 94	eleqtrrd	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to a \in {Base}_{Scalar (R (y))}$
96	90 94	eleqtrrd	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to b \in {Base}_{Scalar (R (y))}$
97	1 20 83 84 85 87 88	prdsbasprj	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to c (y) \in {Base}_{R (y)}$
98		eqid	$⊢ +_{Scalar (R (y))} = +_{Scalar (R (y))}$
99	47 48 49 50 51 98	lmodvsdir	$⊢ (R (y) \in LMod \land (a \in {Base}_{Scalar (R (y))} \land b \in {Base}_{Scalar (R (y))} \land c (y) \in {Base}_{R (y)})) \to (a +_{Scalar (R (y))} b) \cdot_{R (y)} c (y) = (a \cdot_{R (y)} c (y)) +_{R (y)} (b \cdot_{R (y)} c (y))$
100	93 95 96 97 99	syl13anc	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a +_{Scalar (R (y))} b) \cdot_{R (y)} c (y) = (a \cdot_{R (y)} c (y)) +_{R (y)} (b \cdot_{R (y)} c (y))$
101	5	adantlr	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to Scalar (R (y)) = S$
102	101	fveq2d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to +_{Scalar (R (y))} = +_{S}$
103	102	oveqd	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to a +_{Scalar (R (y))} b = a +_{S} b$
104	103	oveq1d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a +_{Scalar (R (y))} b) \cdot_{R (y)} c (y) = (a +_{S} b) \cdot_{R (y)} c (y)$
105	92 100 104	3eqtr2rd	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a +_{S} b) \cdot_{R (y)} c (y) = (a \cdot_{Y} c) (y) +_{R (y)} (b \cdot_{Y} c) (y)$
106	105	mpteq2dva	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to (y \in I ⟼ (a +_{S} b) \cdot_{R (y)} c (y)) = (y \in I ⟼ (a \cdot_{Y} c) (y) +_{R (y)} (b \cdot_{Y} c) (y))$
107	2	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to S \in Ring$
108	24	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to I \in V$
109	40	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to R Fn I$
110		simpr1	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to a \in {Base}_{S}$
111		simpr2	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to b \in {Base}_{S}$
112		eqid	$⊢ +_{S} = +_{S}$
113	22 112	ringacl	$⊢ (S \in Ring \land a \in {Base}_{S} \land b \in {Base}_{S}) \to a +_{S} b \in {Base}_{S}$
114	107 110 111 113	syl3anc	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to a +_{S} b \in {Base}_{S}$
115		simpr3	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to c \in {Base}_{Y}$
116	1 20 21 22 107 108 109 114 115	prdsvscaval	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to (a +_{S} b) \cdot_{Y} c = (y \in I ⟼ (a +_{S} b) \cdot_{R (y)} c (y))$
117	79	3adantr2	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to a \cdot_{Y} c \in {Base}_{Y}$
118	4	adantr	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to R : I ⟶ LMod$
119	1 20 21 22 107 108 118 111 115 101	prdsvscacl	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to b \cdot_{Y} c \in {Base}_{Y}$
120	1 20 107 108 109 117 119 54	prdsplusgval	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to (a \cdot_{Y} c) +_{Y} (b \cdot_{Y} c) = (y \in I ⟼ (a \cdot_{Y} c) (y) +_{R (y)} (b \cdot_{Y} c) (y))$
121	106 116 120	3eqtr4d	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to (a +_{S} b) \cdot_{Y} c = (a \cdot_{Y} c) +_{Y} (b \cdot_{Y} c)$
122	91	oveq2d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to a \cdot_{R (y)} (b \cdot_{Y} c) (y) = a \cdot_{R (y)} (b \cdot_{R (y)} c (y))$
123		eqid	$⊢ \cdot_{Scalar (R (y))} = \cdot_{Scalar (R (y))}$
124	47 49 50 51 123	lmodvsass	$⊢ (R (y) \in LMod \land (a \in {Base}_{Scalar (R (y))} \land b \in {Base}_{Scalar (R (y))} \land c (y) \in {Base}_{R (y)})) \to (a \cdot_{Scalar (R (y))} b) \cdot_{R (y)} c (y) = a \cdot_{R (y)} (b \cdot_{R (y)} c (y))$
125	93 95 96 97 124	syl13anc	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{Scalar (R (y))} b) \cdot_{R (y)} c (y) = a \cdot_{R (y)} (b \cdot_{R (y)} c (y))$
126	101	fveq2d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to \cdot_{Scalar (R (y))} = \cdot_{S}$
127	126	oveqd	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to a \cdot_{Scalar (R (y))} b = a \cdot_{S} b$
128	127	oveq1d	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{Scalar (R (y))} b) \cdot_{R (y)} c (y) = (a \cdot_{S} b) \cdot_{R (y)} c (y)$
129	122 125 128	3eqtr2rd	$⊢ ((φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \land y \in I) \to (a \cdot_{S} b) \cdot_{R (y)} c (y) = a \cdot_{R (y)} (b \cdot_{Y} c) (y)$
130	129	mpteq2dva	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to (y \in I ⟼ (a \cdot_{S} b) \cdot_{R (y)} c (y)) = (y \in I ⟼ a \cdot_{R (y)} (b \cdot_{Y} c) (y))$
131		eqid	$⊢ \cdot_{S} = \cdot_{S}$
132	22 131	ringcl	$⊢ (S \in Ring \land a \in {Base}_{S} \land b \in {Base}_{S}) \to a \cdot_{S} b \in {Base}_{S}$
133	107 110 111 132	syl3anc	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to a \cdot_{S} b \in {Base}_{S}$
134	1 20 21 22 107 108 109 133 115	prdsvscaval	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to (a \cdot_{S} b) \cdot_{Y} c = (y \in I ⟼ (a \cdot_{S} b) \cdot_{R (y)} c (y))$
135	1 20 21 22 107 108 109 110 119	prdsvscaval	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to a \cdot_{Y} (b \cdot_{Y} c) = (y \in I ⟼ a \cdot_{R (y)} (b \cdot_{Y} c) (y))$
136	130 134 135	3eqtr4d	$⊢ (φ \land (a \in {Base}_{S} \land b \in {Base}_{S} \land c \in {Base}_{Y})) \to (a \cdot_{S} b) \cdot_{Y} c = a \cdot_{Y} (b \cdot_{Y} c)$
137	5	fveq2d	$⊢ (φ \land y \in I) \to 1_{Scalar (R (y))} = 1_{S}$
138	137	adantlr	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to 1_{Scalar (R (y))} = 1_{S}$
139	138	oveq1d	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to 1_{Scalar (R (y))} \cdot_{R (y)} a (y) = 1_{S} \cdot_{R (y)} a (y)$
140	32	adantlr	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to R (y) \in LMod$
141	2	ad2antrr	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to S \in Ring$
142	24	ad2antrr	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to I \in V$
143	40	ad2antrr	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to R Fn I$
144		simplr	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to a \in {Base}_{Y}$
145		simpr	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to y \in I$
146	1 20 141 142 143 144 145	prdsbasprj	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to a (y) \in {Base}_{R (y)}$
147		eqid	$⊢ 1_{Scalar (R (y))} = 1_{Scalar (R (y))}$
148	47 49 50 147	lmodvs1	$⊢ (R (y) \in LMod \land a (y) \in {Base}_{R (y)}) \to 1_{Scalar (R (y))} \cdot_{R (y)} a (y) = a (y)$
149	140 146 148	syl2anc	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to 1_{Scalar (R (y))} \cdot_{R (y)} a (y) = a (y)$
150	139 149	eqtr3d	$⊢ ((φ \land a \in {Base}_{Y}) \land y \in I) \to 1_{S} \cdot_{R (y)} a (y) = a (y)$
151	150	mpteq2dva	$⊢ (φ \land a \in {Base}_{Y}) \to (y \in I ⟼ 1_{S} \cdot_{R (y)} a (y)) = (y \in I ⟼ a (y))$
152	2	adantr	$⊢ (φ \land a \in {Base}_{Y}) \to S \in Ring$
153	24	adantr	$⊢ (φ \land a \in {Base}_{Y}) \to I \in V$
154	40	adantr	$⊢ (φ \land a \in {Base}_{Y}) \to R Fn I$
155		eqid	$⊢ 1_{S} = 1_{S}$
156	22 155	ringidcl	$⊢ S \in Ring \to 1_{S} \in {Base}_{S}$
157	2 156	syl	$⊢ φ \to 1_{S} \in {Base}_{S}$
158	157	adantr	$⊢ (φ \land a \in {Base}_{Y}) \to 1_{S} \in {Base}_{S}$
159		simpr	$⊢ (φ \land a \in {Base}_{Y}) \to a \in {Base}_{Y}$
160	1 20 21 22 152 153 154 158 159	prdsvscaval	$⊢ (φ \land a \in {Base}_{Y}) \to 1_{S} \cdot_{Y} a = (y \in I ⟼ 1_{S} \cdot_{R (y)} a (y))$
161	1 20 152 153 154 159	prdsbasfn	$⊢ (φ \land a \in {Base}_{Y}) \to a Fn I$
162		dffn5	$⊢ a Fn I \leftrightarrow a = (y \in I ⟼ a (y))$
163	161 162	sylib	$⊢ (φ \land a \in {Base}_{Y}) \to a = (y \in I ⟼ a (y))$
164	151 160 163	3eqtr4d	$⊢ (φ \land a \in {Base}_{Y}) \to 1_{S} \cdot_{Y} a = a$
165	6 7 9 10 11 12 13 14 2 19 31 82 121 136 164	islmodd	$⊢ φ \to Y \in LMod$

Metamath Proof Explorer

Theorem prdslmodd

Proof