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