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