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