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 grpmgmd 
 |-  ( ph -> R e. Mgm )
47 46 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> R e. Mgm )
48 1 17 39 47 29 31 psraddcl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( y ( +g ` S ) z ) e. ( Base ` S ) )
49 1 15 16 17 35 28 25 48 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 ) ) )
50 21 3adant3r3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) y ) e. ( Base ` S ) )
51 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 ) )
52 1 17 34 39 50 51 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 ) ) )
53 45 49 52 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 ) ) )
54 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` R ) )
55 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) )
56 1 15 16 17 35 28 54 55 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 ) )
57 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` R ) )
58 1 15 16 17 35 28 57 55 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 ) )
59 56 58 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 ) ) )
60 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 )
61 1 16 28 17 55 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 ) )
62 54 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 ) )
63 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 ) )
64 57 63 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 ) )
65 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> R e. Ring )
66 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 ) ) )
67 65 66 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 ) ) )
68 60 61 62 64 67 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 ) ) )
69 60 54 57 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 ) } ) )
70 69 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 ) )
71 59 68 70 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 ) ) )
72 16 34 ringacl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
73 65 54 57 72 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
74 1 15 16 17 35 28 73 55 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 ) )
75 1 15 16 17 65 54 55 psrvscacl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( .s ` S ) z ) e. ( Base ` S ) )
76 1 15 16 17 65 57 55 psrvscacl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( y ( .s ` S ) z ) e. ( Base ` S ) )
77 1 17 34 39 75 76 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 ) ) )
78 71 74 77 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 ) ) )
79 58 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 ) ) )
80 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 ) ) )
81 65 80 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 ) ) )
82 60 62 64 61 81 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 ) ) )
83 60 54 57 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 ) } ) )
84 83 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 ) )
85 79 82 84 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 ) ) )
86 16 35 ringcl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
87 65 54 57 86 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` S ) ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
88 1 15 16 17 35 28 87 55 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 ) )
89 1 15 16 17 35 28 54 76 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 ) ) )
90 85 88 89 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 ) ) )
91 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> R e. Ring )
92 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
93 16 92 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
94 91 93 syl 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( 1r ` R ) e. ( Base ` R ) )
95 simpr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x e. ( Base ` S ) )
96 1 15 16 17 35 28 94 95 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 ) )
97 23 a1i 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
98 1 16 28 17 95 psrelbas 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x : { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } --> ( Base ` R ) )
99 16 35 92 ringlidm 
 |-  ( ( R e. Ring /\ r e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) r ) = r )
100 91 99 sylan 
 |-  ( ( ( ph /\ x e. ( Base ` S ) ) /\ r e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) r ) = r )
101 97 98 94 100 caofid0l 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } X. { ( 1r ` R ) } ) oF ( .r ` R ) x ) = x )
102 96 101 eqtrd 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( 1r ` R ) ( .s ` S ) x ) = x )
103 4 5 6 7 8 9 10 11 3 14 21 53 78 90 102 islmodd 
 |-  ( ph -> S e. LMod )