Metamath Proof Explorer

Theorem psrass1

Description: Associative identity for the ring of power series. (Contributed by Mario Carneiro, 5-Jan-2015)

Ref Expression
Hypotheses psrring.s 
|- S = ( I mPwSer R )
psrring.i 
|- ( ph -> I e. V )
psrring.r 
|- ( ph -> R e. Ring )
psrass.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrass.t 
|- .X. = ( .r ` S )
psrass.b 
|- B = ( Base ` S )
psrass.x 
|- ( ph -> X e. B )
psrass.y 
|- ( ph -> Y e. B )
psrass.z 
|- ( ph -> Z e. B )
Assertion psrass1 
|- ( ph -> ( ( X .X. Y ) .X. Z ) = ( X .X. ( Y .X. Z ) ) )

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 psrass.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
5 psrass.t 
 |-  .X. = ( .r ` S )
6 psrass.b 
 |-  B = ( Base ` S )
7 psrass.x 
 |-  ( ph -> X e. B )
8 psrass.y 
 |-  ( ph -> Y e. B )
9 psrass.z 
 |-  ( ph -> Z e. B )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 1 6 5 3 7 8 psrmulcl 
 |-  ( ph -> ( X .X. Y ) e. B )
12 1 6 5 3 11 9 psrmulcl 
 |-  ( ph -> ( ( X .X. Y ) .X. Z ) e. B )
13 1 10 4 6 12 psrelbas 
 |-  ( ph -> ( ( X .X. Y ) .X. Z ) : D --> ( Base ` R ) )
14 13 ffnd 
 |-  ( ph -> ( ( X .X. Y ) .X. Z ) Fn D )
15 1 6 5 3 8 9 psrmulcl 
 |-  ( ph -> ( Y .X. Z ) e. B )
16 1 6 5 3 7 15 psrmulcl 
 |-  ( ph -> ( X .X. ( Y .X. Z ) ) e. B )
17 1 10 4 6 16 psrelbas 
 |-  ( ph -> ( X .X. ( Y .X. Z ) ) : D --> ( Base ` R ) )
18 17 ffnd 
 |-  ( ph -> ( X .X. ( Y .X. Z ) ) Fn D )
19 eqid 
 |-  { g e. D | g oR <_ x } = { g e. D | g oR <_ x }
20 2 adantr 
 |-  ( ( ph /\ x e. D ) -> I e. V )
21 simpr 
 |-  ( ( ph /\ x e. D ) -> x e. D )
22 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
23 3 22 syl 
 |-  ( ph -> R e. CMnd )
24 23 adantr 
 |-  ( ( ph /\ x e. D ) -> R e. CMnd )
25 3 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> R e. Ring )
26 25 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> R e. Ring )
27 1 10 4 6 7 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
28 27 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> X : D --> ( Base ` R ) )
29 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j e. { g e. D | g oR <_ x } )
30 breq1 
 |-  ( g = j -> ( g oR <_ x <-> j oR <_ x ) )
31 30 elrab 
 |-  ( j e. { g e. D | g oR <_ x } <-> ( j e. D /\ j oR <_ x ) )
32 29 31 sylib 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( j e. D /\ j oR <_ x ) )
33 32 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j e. D )
34 28 33 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( X ` j ) e. ( Base ` R ) )
35 34 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( X ` j ) e. ( Base ` R ) )
36 1 10 4 6 8 psrelbas 
 |-  ( ph -> Y : D --> ( Base ` R ) )
37 36 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> Y : D --> ( Base ` R ) )
38 simpr 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> n e. { h e. D | h oR <_ ( x oF - j ) } )
39 breq1 
 |-  ( h = n -> ( h oR <_ ( x oF - j ) <-> n oR <_ ( x oF - j ) ) )
40 39 elrab 
 |-  ( n e. { h e. D | h oR <_ ( x oF - j ) } <-> ( n e. D /\ n oR <_ ( x oF - j ) ) )
41 38 40 sylib 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( n e. D /\ n oR <_ ( x oF - j ) ) )
42 41 simpld 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> n e. D )
43 37 42 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( Y ` n ) e. ( Base ` R ) )
44 1 10 4 6 9 psrelbas 
 |-  ( ph -> Z : D --> ( Base ` R ) )
45 44 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> Z : D --> ( Base ` R ) )
46 2 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> I e. V )
47 46 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> I e. V )
48 simplr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> x e. D )
49 4 psrbagf 
 |-  ( ( I e. V /\ j e. D ) -> j : I --> NN0 )
50 46 33 49 syl2anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j : I --> NN0 )
51 32 simprd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j oR <_ x )
52 4 psrbagcon 
 |-  ( ( I e. V /\ ( x e. D /\ j : I --> NN0 /\ j oR <_ x ) ) -> ( ( x oF - j ) e. D /\ ( x oF - j ) oR <_ x ) )
53 46 48 50 51 52 syl13anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( x oF - j ) e. D /\ ( x oF - j ) oR <_ x ) )
54 53 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( x oF - j ) e. D )
55 54 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( x oF - j ) e. D )
56 4 psrbagf 
 |-  ( ( I e. V /\ n e. D ) -> n : I --> NN0 )
57 47 42 56 syl2anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> n : I --> NN0 )
58 41 simprd 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> n oR <_ ( x oF - j ) )
59 4 psrbagcon 
 |-  ( ( I e. V /\ ( ( x oF - j ) e. D /\ n : I --> NN0 /\ n oR <_ ( x oF - j ) ) ) -> ( ( ( x oF - j ) oF - n ) e. D /\ ( ( x oF - j ) oF - n ) oR <_ ( x oF - j ) ) )
60 47 55 57 58 59 syl13anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( ( ( x oF - j ) oF - n ) e. D /\ ( ( x oF - j ) oF - n ) oR <_ ( x oF - j ) ) )
61 60 simpld 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( ( x oF - j ) oF - n ) e. D )
62 45 61 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( Z ` ( ( x oF - j ) oF - n ) ) e. ( Base ` R ) )
63 eqid 
 |-  ( .r ` R ) = ( .r ` R )
64 10 63 ringcl 
 |-  ( ( R e. Ring /\ ( Y ` n ) e. ( Base ` R ) /\ ( Z ` ( ( x oF - j ) oF - n ) ) e. ( Base ` R ) ) -> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) e. ( Base ` R ) )
65 26 43 62 64 syl3anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) e. ( Base ` R ) )
66 10 63 ringcl 
 |-  ( ( R e. Ring /\ ( X ` j ) e. ( Base ` R ) /\ ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) e. ( Base ` R ) ) -> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) e. ( Base ` R ) )
67 26 35 65 66 syl3anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) -> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) e. ( Base ` R ) )
68 67 anasss 
 |-  ( ( ( ph /\ x e. D ) /\ ( j e. { g e. D | g oR <_ x } /\ n e. { h e. D | h oR <_ ( x oF - j ) } ) ) -> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) e. ( Base ` R ) )
69 fveq2 
 |-  ( n = ( k oF - j ) -> ( Y ` n ) = ( Y ` ( k oF - j ) ) )
70 oveq2 
 |-  ( n = ( k oF - j ) -> ( ( x oF - j ) oF - n ) = ( ( x oF - j ) oF - ( k oF - j ) ) )
71 70 fveq2d 
 |-  ( n = ( k oF - j ) -> ( Z ` ( ( x oF - j ) oF - n ) ) = ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) )
72 69 71 oveq12d 
 |-  ( n = ( k oF - j ) -> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) = ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) )
73 72 oveq2d 
 |-  ( n = ( k oF - j ) -> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) = ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) )
74 4 19 20 21 10 24 68 73 psrass1lem 
 |-  ( ( ph /\ x e. D ) -> ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) ) ) ) ) = ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) ) ) ) )
75 7 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> X e. B )
76 8 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> Y e. B )
77 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k e. { g e. D | g oR <_ x } )
78 breq1 
 |-  ( g = k -> ( g oR <_ x <-> k oR <_ x ) )
79 78 elrab 
 |-  ( k e. { g e. D | g oR <_ x } <-> ( k e. D /\ k oR <_ x ) )
80 77 79 sylib 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( k e. D /\ k oR <_ x ) )
81 80 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k e. D )
82 1 6 63 5 4 75 76 81 psrmulval 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( ( X .X. Y ) ` k ) = ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ) ) )
83 82 oveq1d 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( ( ( X .X. Y ) ` k ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) = ( ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) )
84 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
85 eqid 
 |-  ( +g ` R ) = ( +g ` R )
86 3 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> R e. Ring )
87 2 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> I e. V )
88 4 psrbaglefi 
 |-  ( ( I e. V /\ k e. D ) -> { h e. D | h oR <_ k } e. Fin )
89 87 81 88 syl2anc 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> { h e. D | h oR <_ k } e. Fin )
90 44 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> Z : D --> ( Base ` R ) )
91 simplr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> x e. D )
92 4 psrbagf 
 |-  ( ( I e. V /\ k e. D ) -> k : I --> NN0 )
93 87 81 92 syl2anc 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k : I --> NN0 )
94 80 simprd 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k oR <_ x )
95 4 psrbagcon 
 |-  ( ( I e. V /\ ( x e. D /\ k : I --> NN0 /\ k oR <_ x ) ) -> ( ( x oF - k ) e. D /\ ( x oF - k ) oR <_ x ) )
96 87 91 93 94 95 syl13anc 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( ( x oF - k ) e. D /\ ( x oF - k ) oR <_ x ) )
97 96 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( x oF - k ) e. D )
98 90 97 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( Z ` ( x oF - k ) ) e. ( Base ` R ) )
99 86 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> R e. Ring )
100 27 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> X : D --> ( Base ` R ) )
101 simpr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> j e. { h e. D | h oR <_ k } )
102 breq1 
 |-  ( h = j -> ( h oR <_ k <-> j oR <_ k ) )
103 102 elrab 
 |-  ( j e. { h e. D | h oR <_ k } <-> ( j e. D /\ j oR <_ k ) )
104 101 103 sylib 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( j e. D /\ j oR <_ k ) )
105 104 simpld 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> j e. D )
106 100 105 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( X ` j ) e. ( Base ` R ) )
107 36 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> Y : D --> ( Base ` R ) )
108 87 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> I e. V )
109 81 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> k e. D )
110 108 105 49 syl2anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> j : I --> NN0 )
111 104 simprd 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> j oR <_ k )
112 4 psrbagcon 
 |-  ( ( I e. V /\ ( k e. D /\ j : I --> NN0 /\ j oR <_ k ) ) -> ( ( k oF - j ) e. D /\ ( k oF - j ) oR <_ k ) )
113 108 109 110 111 112 syl13anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( k oF - j ) e. D /\ ( k oF - j ) oR <_ k ) )
114 113 simpld 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( k oF - j ) e. D )
115 107 114 ffvelrnd 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( Y ` ( k oF - j ) ) e. ( Base ` R ) )
116 10 63 ringcl 
 |-  ( ( R e. Ring /\ ( X ` j ) e. ( Base ` R ) /\ ( Y ` ( k oF - j ) ) e. ( Base ` R ) ) -> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) e. ( Base ` R ) )
117 99 106 115 116 syl3anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) e. ( Base ` R ) )
118 eqid 
 |-  ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ) = ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) )
119 fvex 
 |-  ( 0g ` R ) e. _V
120 119 a1i 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( 0g ` R ) e. _V )
121 118 89 117 120 fsuppmptdm 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ) finSupp ( 0g ` R ) )
122 10 84 85 63 86 89 98 117 121 gsummulc1 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) ) = ( ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) )
123 98 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( Z ` ( x oF - k ) ) e. ( Base ` R ) )
124 10 63 ringass 
 |-  ( ( R e. Ring /\ ( ( X ` j ) e. ( Base ` R ) /\ ( Y ` ( k oF - j ) ) e. ( Base ` R ) /\ ( Z ` ( x oF - k ) ) e. ( Base ` R ) ) ) -> ( ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) = ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) )
125 99 106 115 123 124 syl13anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) = ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) )
126 4 psrbagf 
 |-  ( ( I e. V /\ x e. D ) -> x : I --> NN0 )
127 2 126 sylan 
 |-  ( ( ph /\ x e. D ) -> x : I --> NN0 )
128 127 ad2antrr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> x : I --> NN0 )
129 128 ffvelrnda 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) /\ z e. I ) -> ( x ` z ) e. NN0 )
130 93 adantr 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> k : I --> NN0 )
131 130 ffvelrnda 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) /\ z e. I ) -> ( k ` z ) e. NN0 )
132 110 ffvelrnda 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) /\ z e. I ) -> ( j ` z ) e. NN0 )
133 nn0cn 
 |-  ( ( x ` z ) e. NN0 -> ( x ` z ) e. CC )
134 nn0cn 
 |-  ( ( k ` z ) e. NN0 -> ( k ` z ) e. CC )
135 nn0cn 
 |-  ( ( j ` z ) e. NN0 -> ( j ` z ) e. CC )
136 nnncan2 
 |-  ( ( ( x ` z ) e. CC /\ ( k ` z ) e. CC /\ ( j ` z ) e. CC ) -> ( ( ( x ` z ) - ( j ` z ) ) - ( ( k ` z ) - ( j ` z ) ) ) = ( ( x ` z ) - ( k ` z ) ) )
137 133 134 135 136 syl3an 
 |-  ( ( ( x ` z ) e. NN0 /\ ( k ` z ) e. NN0 /\ ( j ` z ) e. NN0 ) -> ( ( ( x ` z ) - ( j ` z ) ) - ( ( k ` z ) - ( j ` z ) ) ) = ( ( x ` z ) - ( k ` z ) ) )
138 129 131 132 137 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) /\ z e. I ) -> ( ( ( x ` z ) - ( j ` z ) ) - ( ( k ` z ) - ( j ` z ) ) ) = ( ( x ` z ) - ( k ` z ) ) )
139 138 mpteq2dva 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( z e. I |-> ( ( ( x ` z ) - ( j ` z ) ) - ( ( k ` z ) - ( j ` z ) ) ) ) = ( z e. I |-> ( ( x ` z ) - ( k ` z ) ) ) )
140 ovexd 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) /\ z e. I ) -> ( ( x ` z ) - ( j ` z ) ) e. _V )
141 ovexd 
 |-  ( ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) /\ z e. I ) -> ( ( k ` z ) - ( j ` z ) ) e. _V )
142 128 feqmptd 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> x = ( z e. I |-> ( x ` z ) ) )
143 110 feqmptd 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> j = ( z e. I |-> ( j ` z ) ) )
144 108 129 132 142 143 offval2 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( x oF - j ) = ( z e. I |-> ( ( x ` z ) - ( j ` z ) ) ) )
145 130 feqmptd 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> k = ( z e. I |-> ( k ` z ) ) )
146 108 131 132 145 143 offval2 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( k oF - j ) = ( z e. I |-> ( ( k ` z ) - ( j ` z ) ) ) )
147 108 140 141 144 146 offval2 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( x oF - j ) oF - ( k oF - j ) ) = ( z e. I |-> ( ( ( x ` z ) - ( j ` z ) ) - ( ( k ` z ) - ( j ` z ) ) ) ) )
148 108 129 131 142 145 offval2 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( x oF - k ) = ( z e. I |-> ( ( x ` z ) - ( k ` z ) ) ) )
149 139 147 148 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( x oF - j ) oF - ( k oF - j ) ) = ( x oF - k ) )
150 149 fveq2d 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) = ( Z ` ( x oF - k ) ) )
151 150 oveq2d 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) = ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) )
152 151 oveq2d 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) = ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) )
153 125 152 eqtr4d 
 |-  ( ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) /\ j e. { h e. D | h oR <_ k } ) -> ( ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) = ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) )
154 153 mpteq2dva 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( j e. { h e. D | h oR <_ k } |-> ( ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) = ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) ) )
155 154 oveq2d 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( ( X ` j ) ( .r ` R ) ( Y ` ( k oF - j ) ) ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) ) = ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) ) ) )
156 83 122 155 3eqtr2d 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( ( ( X .X. Y ) ` k ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) = ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) ) ) )
157 156 mpteq2dva 
 |-  ( ( ph /\ x e. D ) -> ( k e. { g e. D | g oR <_ x } |-> ( ( ( X .X. Y ) ` k ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) = ( k e. { g e. D | g oR <_ x } |-> ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) ) ) ) )
158 157 oveq2d 
 |-  ( ( ph /\ x e. D ) -> ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( ( ( X .X. Y ) ` k ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) ) = ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( R gsum ( j e. { h e. D | h oR <_ k } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` ( k oF - j ) ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - ( k oF - j ) ) ) ) ) ) ) ) ) )
159 8 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> Y e. B )
160 9 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> Z e. B )
161 1 6 63 5 4 159 160 54 psrmulval 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( Y .X. Z ) ` ( x oF - j ) ) = ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) )
162 161 oveq2d 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( X ` j ) ( .r ` R ) ( ( Y .X. Z ) ` ( x oF - j ) ) ) = ( ( X ` j ) ( .r ` R ) ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) ) )
163 4 psrbaglefi 
 |-  ( ( I e. V /\ ( x oF - j ) e. D ) -> { h e. D | h oR <_ ( x oF - j ) } e. Fin )
164 46 54 163 syl2anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> { h e. D | h oR <_ ( x oF - j ) } e. Fin )
165 ovex 
 |-  ( NN0 ^m I ) e. _V
166 4 165 rab2ex 
 |-  { h e. D | h oR <_ ( x oF - j ) } e. _V
167 166 mptex 
 |-  ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) e. _V
168 funmpt 
 |-  Fun ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) )
169 167 168 119 3pm3.2i 
 |-  ( ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) e. _V /\ Fun ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) /\ ( 0g ` R ) e. _V )
170 169 a1i 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) e. _V /\ Fun ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) /\ ( 0g ` R ) e. _V ) )
171 suppssdm 
 |-  ( ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) supp ( 0g ` R ) ) C_ dom ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) )
172 eqid 
 |-  ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) = ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) )
173 172 dmmptss 
 |-  dom ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) C_ { h e. D | h oR <_ ( x oF - j ) }
174 171 173 sstri 
 |-  ( ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) supp ( 0g ` R ) ) C_ { h e. D | h oR <_ ( x oF - j ) }
175 174 a1i 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) supp ( 0g ` R ) ) C_ { h e. D | h oR <_ ( x oF - j ) } )
176 suppssfifsupp 
 |-  ( ( ( ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) e. _V /\ Fun ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( { h e. D | h oR <_ ( x oF - j ) } e. Fin /\ ( ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) supp ( 0g ` R ) ) C_ { h e. D | h oR <_ ( x oF - j ) } ) ) -> ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) finSupp ( 0g ` R ) )
177 170 164 175 176 syl12anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) finSupp ( 0g ` R ) )
178 10 84 85 63 25 164 34 65 177 gsummulc2 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) ) = ( ( X ` j ) ( .r ` R ) ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) ) )
179 162 178 eqtr4d 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( X ` j ) ( .r ` R ) ( ( Y .X. Z ) ` ( x oF - j ) ) ) = ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) ) )
180 179 mpteq2dva 
 |-  ( ( ph /\ x e. D ) -> ( j e. { g e. D | g oR <_ x } |-> ( ( X ` j ) ( .r ` R ) ( ( Y .X. Z ) ` ( x oF - j ) ) ) ) = ( j e. { g e. D | g oR <_ x } |-> ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) ) ) )
181 180 oveq2d 
 |-  ( ( ph /\ x e. D ) -> ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( ( X ` j ) ( .r ` R ) ( ( Y .X. Z ) ` ( x oF - j ) ) ) ) ) = ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( R gsum ( n e. { h e. D | h oR <_ ( x oF - j ) } |-> ( ( X ` j ) ( .r ` R ) ( ( Y ` n ) ( .r ` R ) ( Z ` ( ( x oF - j ) oF - n ) ) ) ) ) ) ) ) )
182 74 158 181 3eqtr4d 
 |-  ( ( ph /\ x e. D ) -> ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( ( ( X .X. Y ) ` k ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) ) = ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( ( X ` j ) ( .r ` R ) ( ( Y .X. Z ) ` ( x oF - j ) ) ) ) ) )
183 11 adantr 
 |-  ( ( ph /\ x e. D ) -> ( X .X. Y ) e. B )
184 9 adantr 
 |-  ( ( ph /\ x e. D ) -> Z e. B )
185 1 6 63 5 4 183 184 21 psrmulval 
 |-  ( ( ph /\ x e. D ) -> ( ( ( X .X. Y ) .X. Z ) ` x ) = ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( ( ( X .X. Y ) ` k ) ( .r ` R ) ( Z ` ( x oF - k ) ) ) ) ) )
186 7 adantr 
 |-  ( ( ph /\ x e. D ) -> X e. B )
187 15 adantr 
 |-  ( ( ph /\ x e. D ) -> ( Y .X. Z ) e. B )
188 1 6 63 5 4 186 187 21 psrmulval 
 |-  ( ( ph /\ x e. D ) -> ( ( X .X. ( Y .X. Z ) ) ` x ) = ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( ( X ` j ) ( .r ` R ) ( ( Y .X. Z ) ` ( x oF - j ) ) ) ) ) )
189 182 185 188 3eqtr4d 
 |-  ( ( ph /\ x e. D ) -> ( ( ( X .X. Y ) .X. Z ) ` x ) = ( ( X .X. ( Y .X. Z ) ) ` x ) )
190 14 18 189 eqfnfvd 
 |-  ( ph -> ( ( X .X. Y ) .X. Z ) = ( X .X. ( Y .X. Z ) ) )