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

Metamath Proof Explorer

Theorem prdslmodd

Proof