Metamath Proof Explorer

Theorem psrlmod

Description: The ring of power series is a left module. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrring.s 
|- S = ( I mPwSer R )
psrring.i 
|- ( ph -> I e. V )
psrring.r 
|- ( ph -> R e. Ring )
Assertion psrlmod 
|- ( ph -> S e. LMod )

Proof

Step Hyp Ref Expression
1 psrring.s 
 |-  S = ( I mPwSer R )
2 psrring.i 
 |-  ( ph -> I e. V )
3 psrring.r 
 |-  ( ph -> R e. Ring )
4 eqidd 
 |-  ( ph -> ( Base ` S ) = ( Base ` S ) )
5 eqidd 
 |-  ( ph -> ( +g ` S ) = ( +g ` S ) )
6 1 2 3 psrsca 
 |-  ( ph -> R = ( Scalar ` S ) )
7 eqidd 
 |-  ( ph -> ( .s ` S ) = ( .s ` S ) )
8 eqidd 
 |-  ( ph -> ( Base ` R ) = ( Base ` R ) )
9 eqidd 
 |-  ( ph -> ( +g ` R ) = ( +g ` R ) )
10 eqidd 
 |-  ( ph -> ( .r ` R ) = ( .r ` R ) )
11 eqidd 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` R ) )
12 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
13 3 12 syl 
 |-  ( ph -> R e. Grp )
14 1 2 13 psrgrp 
 |-  ( ph -> S e. Grp )
15 eqid 
 |-  ( .s ` S ) = ( .s ` S )
16 eqid 
 |-  ( Base ` R ) = ( Base ` R )
17 eqid 
 |-  ( Base ` S ) = ( Base ` S )
18 3 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` S ) ) -> R e. Ring )
19 simp2 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` R ) )
20 simp3 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
21 1 15 16 17 18 19 20 psrvscacl 
 |-  ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` S ) ) -> ( x ( .s ` S ) y ) e. ( Base ` S ) )
22 ovex 
 |-  ( NN0 ^m I ) e. _V
23 22 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
24 23 a1i 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
25 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` R ) )
26 fconst6g 
 |-  ( x e. ( Base ` R ) -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
27 25 26 syl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
28 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
29 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
30 1 16 28 17 29 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
31 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) )
32 1 16 28 17 31 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
33 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Ring )
34 eqid 
 |-  ( +g ` R ) = ( +g ` R )
35 eqid 
 |-  ( .r ` R ) = ( .r ` R )
36 16 34 35 ringdi 
 |-  ( ( R e. Ring /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( r ( .r ` R ) ( s ( +g ` R ) t ) ) = ( ( r ( .r ` R ) s ) ( +g ` R ) ( r ( .r ` R ) t ) ) )
37 33 36 sylan 
 |-  ( ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( r ( .r ` R ) ( s ( +g ` R ) t ) ) = ( ( r ( .r ` R ) s ) ( +g ` R ) ( r ( .r ` R ) t ) ) )
38 24 27 30 32 37 caofdi 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y oF ( +g ` R ) z ) ) = ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) y ) oF ( +g ` R ) ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) z ) ) )
39 eqid 
 |-  ( +g ` S ) = ( +g ` S )
40 1 17 34 39 29 31 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( +g ` S ) z ) = ( y oF ( +g ` R ) z ) )
41 40 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y ( +g ` S ) z ) ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y oF ( +g ` R ) z ) ) )
42 1 15 16 17 35 28 25 29 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) y ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) y ) )
43 1 15 16 17 35 28 25 31 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) z ) )
44 42 43 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .s ` S ) y ) oF ( +g ` R ) ( x ( .s ` S ) z ) ) = ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) y ) oF ( +g ` R ) ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) z ) ) )
45 38 41 44 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y ( +g ` S ) z ) ) = ( ( x ( .s ` S ) y ) oF ( +g ` R ) ( x ( .s ` S ) z ) ) )
46 13 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Grp )
47 1 17 39 46 29 31 psraddcl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( +g ` S ) z ) e. ( Base ` S ) )
48 1 15 16 17 35 28 25 47 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) ( y ( +g ` S ) z ) ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y ( +g ` S ) z ) ) )
49 21 3adant3r3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) y ) e. ( Base ` S ) )
50 1 15 16 17 33 25 31 psrvscacl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) z ) e. ( Base ` S ) )
51 1 17 34 39 49 50 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .s ` S ) y ) ( +g ` S ) ( x ( .s ` S ) z ) ) = ( ( x ( .s ` S ) y ) oF ( +g ` R ) ( x ( .s ` S ) z ) ) )
52 45 48 51 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) ( y ( +g ` S ) z ) ) = ( ( x ( .s ` S ) y ) ( +g ` S ) ( x ( .s ` S ) z ) ) )
53 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` R ) )
54 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) )
55 1 15 16 17 35 28 53 54 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) z ) )
56 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` R ) )
57 1 15 16 17 35 28 56 54 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( y ( .s ` S ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) oF ( .r ` R ) z ) )
58 55 57 oveq12d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .s ` S ) z ) oF ( +g ` R ) ( y ( .s ` S ) z ) ) = ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) z ) oF ( +g ` R ) ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) oF ( .r ` R ) z ) ) )
59 23 a1i 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
60 1 16 28 17 54 psrelbas 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> z : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
61 53 26 syl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
62 fconst6g 
 |-  ( y e. ( Base ` R ) -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
63 56 62 syl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
64 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> R e. Ring )
65 16 34 35 ringdir 
 |-  ( ( R e. Ring /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( +g ` R ) s ) ( .r ` R ) t ) = ( ( r ( .r ` R ) t ) ( +g ` R ) ( s ( .r ` R ) t ) ) )
66 64 65 sylan 
 |-  ( ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( +g ` R ) s ) ( .r ` R ) t ) = ( ( r ( .r ` R ) t ) ( +g ` R ) ( s ( .r ` R ) t ) ) )
67 59 60 61 63 66 caofdir 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( +g ` R ) ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) ) oF ( .r ` R ) z ) = ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) z ) oF ( +g ` R ) ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) oF ( .r ` R ) z ) ) )
68 59 53 56 ofc12 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( +g ` R ) ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) ) = ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( +g ` R ) y ) } ) )
69 68 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( +g ` R ) ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) ) oF ( .r ` R ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( +g ` R ) y ) } ) oF ( .r ` R ) z ) )
70 58 67 69 3eqtr2rd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( +g ` R ) y ) } ) oF ( .r ` R ) z ) = ( ( x ( .s ` S ) z ) oF ( +g ` R ) ( y ( .s ` S ) z ) ) )
71 16 34 ringacl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
72 64 53 56 71 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
73 1 15 16 17 35 28 72 54 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` R ) y ) ( .s ` S ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( +g ` R ) y ) } ) oF ( .r ` R ) z ) )
74 1 15 16 17 64 53 54 psrvscacl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) z ) e. ( Base ` S ) )
75 1 15 16 17 64 56 54 psrvscacl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( y ( .s ` S ) z ) e. ( Base ` S ) )
76 1 17 34 39 74 75 psradd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .s ` S ) z ) ( +g ` S ) ( y ( .s ` S ) z ) ) = ( ( x ( .s ` S ) z ) oF ( +g ` R ) ( y ( .s ` S ) z ) ) )
77 70 73 76 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` R ) y ) ( .s ` S ) z ) = ( ( x ( .s ` S ) z ) ( +g ` S ) ( y ( .s ` S ) z ) ) )
78 57 oveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y ( .s ` S ) z ) ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) oF ( .r ` R ) z ) ) )
79 16 35 ringass 
 |-  ( ( R e. Ring /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( .r ` R ) s ) ( .r ` R ) t ) = ( r ( .r ` R ) ( s ( .r ` R ) t ) ) )
80 64 79 sylan 
 |-  ( ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) /\ ( r e. ( Base ` R ) /\ s e. ( Base ` R ) /\ t e. ( Base ` R ) ) ) -> ( ( r ( .r ` R ) s ) ( .r ` R ) t ) = ( r ( .r ` R ) ( s ( .r ` R ) t ) ) )
81 59 61 63 60 80 caofass 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) ) oF ( .r ` R ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) oF ( .r ` R ) z ) ) )
82 59 53 56 ofc12 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) ) = ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( .r ` R ) y ) } ) )
83 82 oveq1d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { y } ) ) oF ( .r ` R ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( .r ` R ) y ) } ) oF ( .r ` R ) z ) )
84 78 81 83 3eqtr2rd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( .r ` R ) y ) } ) oF ( .r ` R ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y ( .s ` S ) z ) ) )
85 16 35 ringcl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
86 64 53 56 85 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
87 1 15 16 17 35 28 86 54 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .r ` R ) y ) ( .s ` S ) z ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( x ( .r ` R ) y ) } ) oF ( .r ` R ) z ) )
88 1 15 16 17 35 28 53 75 psrvsca 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) ( y ( .s ` S ) z ) ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { x } ) oF ( .r ` R ) ( y ( .s ` S ) z ) ) )
89 84 87 88 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .r ` R ) y ) ( .s ` S ) z ) = ( x ( .s ` S ) ( y ( .s ` S ) z ) ) )
90 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> R e. Ring )
91 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
92 16 91 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
93 90 92 syl 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( 1r ` R ) e. ( Base ` R ) )
94 simpr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x e. ( Base ` S ) )
95 1 15 16 17 35 28 93 94 psrvsca 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( 1r ` R ) ( .s ` S ) x ) = ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 1r ` R ) } ) oF ( .r ` R ) x ) )
96 23 a1i 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
97 1 16 28 17 94 psrelbas 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
98 16 35 91 ringlidm 
 |-  ( ( R e. Ring /\ r e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) r ) = r )
99 90 98 sylan 
 |-  ( ( ( ph /\ x e. ( Base ` S ) ) /\ r e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) r ) = r )
100 96 97 93 99 caofid0l 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 1r ` R ) } ) oF ( .r ` R ) x ) = x )
101 95 100 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( 1r ` R ) ( .s ` S ) x ) = x )
102 4 5 6 7 8 9 10 11 3 14 21 52 77 89 101 islmodd 
 |-  ( ph -> S e. LMod )