Metamath Proof Explorer

Theorem 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 Xs_ R )
prdslmodd.s 
|- ( ph -> S e. Ring )
prdslmodd.i 
|- ( ph -> I e. V )
prdslmodd.rm 
|- ( ph -> R : I --> LMod )
prdslmodd.rs 
|- ( ( ph /\ y e. I ) -> ( Scalar ` ( R ` y ) ) = S )
Assertion prdslmodd 
|- ( ph -> Y e. LMod )

Proof

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