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