Metamath Proof Explorer

Theorem psrcom

Description: Commutative law for the ring of power series. (Contributed by Mario Carneiro, 7-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 )
psrcom.c 
|- ( ph -> R e. CRing )
Assertion psrcom 
|- ( ph -> ( X .X. Y ) = ( Y .X. X ) )

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 psrcom.c 
 |-  ( ph -> R e. CRing )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
12 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
13 3 12 syl 
 |-  ( ph -> R e. CMnd )
14 13 adantr 
 |-  ( ( ph /\ x e. D ) -> R e. CMnd )
15 4 psrbaglefi 
 |-  ( ( I e. V /\ x e. D ) -> { g e. D | g oR <_ x } e. Fin )
16 2 15 sylan 
 |-  ( ( ph /\ x e. D ) -> { g e. D | g oR <_ x } e. Fin )
17 3 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> R e. Ring )
18 1 10 4 6 7 psrelbas 
 |-  ( ph -> X : D --> ( Base ` R ) )
19 18 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> X : D --> ( Base ` R ) )
20 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k e. { g e. D | g oR <_ x } )
21 breq1 
 |-  ( g = k -> ( g oR <_ x <-> k oR <_ x ) )
22 21 elrab 
 |-  ( k e. { g e. D | g oR <_ x } <-> ( k e. D /\ k oR <_ x ) )
23 20 22 sylib 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( k e. D /\ k oR <_ x ) )
24 23 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k e. D )
25 19 24 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( X ` k ) e. ( Base ` R ) )
26 1 10 4 6 8 psrelbas 
 |-  ( ph -> Y : D --> ( Base ` R ) )
27 26 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> Y : D --> ( Base ` R ) )
28 2 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> I e. V )
29 simplr 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> x e. D )
30 4 psrbagf 
 |-  ( ( I e. V /\ k e. D ) -> k : I --> NN0 )
31 28 24 30 syl2anc 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k : I --> NN0 )
32 23 simprd 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> k oR <_ x )
33 4 psrbagcon 
 |-  ( ( I e. V /\ ( x e. D /\ k : I --> NN0 /\ k oR <_ x ) ) -> ( ( x oF - k ) e. D /\ ( x oF - k ) oR <_ x ) )
34 28 29 31 32 33 syl13anc 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( ( x oF - k ) e. D /\ ( x oF - k ) oR <_ x ) )
35 34 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( x oF - k ) e. D )
36 27 35 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( Y ` ( x oF - k ) ) e. ( Base ` R ) )
37 eqid 
 |-  ( .r ` R ) = ( .r ` R )
38 10 37 ringcl 
 |-  ( ( R e. Ring /\ ( X ` k ) e. ( Base ` R ) /\ ( Y ` ( x oF - k ) ) e. ( Base ` R ) ) -> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) e. ( Base ` R ) )
39 17 25 36 38 syl3anc 
 |-  ( ( ( ph /\ x e. D ) /\ k e. { g e. D | g oR <_ x } ) -> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) e. ( Base ` R ) )
40 39 fmpttd 
 |-  ( ( ph /\ x e. D ) -> ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) : { g e. D | g oR <_ x } --> ( Base ` R ) )
41 ovex 
 |-  ( NN0 ^m I ) e. _V
42 4 41 rabex2 
 |-  D e. _V
43 42 a1i 
 |-  ( ( ph /\ x e. D ) -> D e. _V )
44 rabexg 
 |-  ( D e. _V -> { g e. D | g oR <_ x } e. _V )
45 43 44 syl 
 |-  ( ( ph /\ x e. D ) -> { g e. D | g oR <_ x } e. _V )
46 45 mptexd 
 |-  ( ( ph /\ x e. D ) -> ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) e. _V )
47 funmpt 
 |-  Fun ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) )
48 47 a1i 
 |-  ( ( ph /\ x e. D ) -> Fun ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) )
49 fvexd 
 |-  ( ( ph /\ x e. D ) -> ( 0g ` R ) e. _V )
50 suppssdm 
 |-  ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) supp ( 0g ` R ) ) C_ dom ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) )
51 eqid 
 |-  ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) = ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) )
52 51 dmmptss 
 |-  dom ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) C_ { g e. D | g oR <_ x }
53 50 52 sstri 
 |-  ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) supp ( 0g ` R ) ) C_ { g e. D | g oR <_ x }
54 53 a1i 
 |-  ( ( ph /\ x e. D ) -> ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) supp ( 0g ` R ) ) C_ { g e. D | g oR <_ x } )
55 suppssfifsupp 
 |-  ( ( ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) e. _V /\ Fun ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( { g e. D | g oR <_ x } e. Fin /\ ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) supp ( 0g ` R ) ) C_ { g e. D | g oR <_ x } ) ) -> ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) finSupp ( 0g ` R ) )
56 46 48 49 16 54 55 syl32anc 
 |-  ( ( ph /\ x e. D ) -> ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) finSupp ( 0g ` R ) )
57 eqid 
 |-  { g e. D | g oR <_ x } = { g e. D | g oR <_ x }
58 4 57 psrbagconf1o 
 |-  ( ( I e. V /\ x e. D ) -> ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) : { g e. D | g oR <_ x } -1-1-onto-> { g e. D | g oR <_ x } )
59 2 58 sylan 
 |-  ( ( ph /\ x e. D ) -> ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) : { g e. D | g oR <_ x } -1-1-onto-> { g e. D | g oR <_ x } )
60 10 11 14 16 40 56 59 gsumf1o 
 |-  ( ( ph /\ x e. D ) -> ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) ) = ( R gsum ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) o. ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) ) ) )
61 2 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> I e. V )
62 simplr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> x e. D )
63 simpr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j e. { g e. D | g oR <_ x } )
64 4 57 psrbagconcl 
 |-  ( ( I e. V /\ x e. D /\ j e. { g e. D | g oR <_ x } ) -> ( x oF - j ) e. { g e. D | g oR <_ x } )
65 61 62 63 64 syl3anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( x oF - j ) e. { g e. D | g oR <_ x } )
66 eqidd 
 |-  ( ( ph /\ x e. D ) -> ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) = ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) )
67 eqidd 
 |-  ( ( ph /\ x e. D ) -> ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) = ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) )
68 fveq2 
 |-  ( k = ( x oF - j ) -> ( X ` k ) = ( X ` ( x oF - j ) ) )
69 oveq2 
 |-  ( k = ( x oF - j ) -> ( x oF - k ) = ( x oF - ( x oF - j ) ) )
70 69 fveq2d 
 |-  ( k = ( x oF - j ) -> ( Y ` ( x oF - k ) ) = ( Y ` ( x oF - ( x oF - j ) ) ) )
71 68 70 oveq12d 
 |-  ( k = ( x oF - j ) -> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) = ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` ( x oF - ( x oF - j ) ) ) ) )
72 65 66 67 71 fmptco 
 |-  ( ( ph /\ x e. D ) -> ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) o. ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) ) = ( j e. { g e. D | g oR <_ x } |-> ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` ( x oF - ( x oF - j ) ) ) ) ) )
73 4 psrbagf 
 |-  ( ( I e. V /\ x e. D ) -> x : I --> NN0 )
74 2 73 sylan 
 |-  ( ( ph /\ x e. D ) -> x : I --> NN0 )
75 74 adantr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> x : I --> NN0 )
76 75 ffvelrnda 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ z e. I ) -> ( x ` z ) e. NN0 )
77 breq1 
 |-  ( g = j -> ( g oR <_ x <-> j oR <_ x ) )
78 77 elrab 
 |-  ( j e. { g e. D | g oR <_ x } <-> ( j e. D /\ j oR <_ x ) )
79 63 78 sylib 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( j e. D /\ j oR <_ x ) )
80 79 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j e. D )
81 4 psrbagf 
 |-  ( ( I e. V /\ j e. D ) -> j : I --> NN0 )
82 61 80 81 syl2anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j : I --> NN0 )
83 82 ffvelrnda 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ z e. I ) -> ( j ` z ) e. NN0 )
84 nn0cn 
 |-  ( ( x ` z ) e. NN0 -> ( x ` z ) e. CC )
85 nn0cn 
 |-  ( ( j ` z ) e. NN0 -> ( j ` z ) e. CC )
86 nncan 
 |-  ( ( ( x ` z ) e. CC /\ ( j ` z ) e. CC ) -> ( ( x ` z ) - ( ( x ` z ) - ( j ` z ) ) ) = ( j ` z ) )
87 84 85 86 syl2an 
 |-  ( ( ( x ` z ) e. NN0 /\ ( j ` z ) e. NN0 ) -> ( ( x ` z ) - ( ( x ` z ) - ( j ` z ) ) ) = ( j ` z ) )
88 76 83 87 syl2anc 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ z e. I ) -> ( ( x ` z ) - ( ( x ` z ) - ( j ` z ) ) ) = ( j ` z ) )
89 88 mpteq2dva 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( z e. I |-> ( ( x ` z ) - ( ( x ` z ) - ( j ` z ) ) ) ) = ( z e. I |-> ( j ` z ) ) )
90 ovex 
 |-  ( ( x ` z ) - ( j ` z ) ) e. _V
91 90 a1i 
 |-  ( ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) /\ z e. I ) -> ( ( x ` z ) - ( j ` z ) ) e. _V )
92 75 feqmptd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> x = ( z e. I |-> ( x ` z ) ) )
93 82 feqmptd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j = ( z e. I |-> ( j ` z ) ) )
94 61 76 83 92 93 offval2 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( x oF - j ) = ( z e. I |-> ( ( x ` z ) - ( j ` z ) ) ) )
95 61 76 91 92 94 offval2 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( x oF - ( x oF - j ) ) = ( z e. I |-> ( ( x ` z ) - ( ( x ` z ) - ( j ` z ) ) ) ) )
96 89 95 93 3eqtr4d 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( x oF - ( x oF - j ) ) = j )
97 96 fveq2d 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( Y ` ( x oF - ( x oF - j ) ) ) = ( Y ` j ) )
98 97 oveq2d 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` ( x oF - ( x oF - j ) ) ) ) = ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` j ) ) )
99 9 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> R e. CRing )
100 18 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> X : D --> ( Base ` R ) )
101 79 simprd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> j oR <_ x )
102 4 psrbagcon 
 |-  ( ( I e. V /\ ( x e. D /\ j : I --> NN0 /\ j oR <_ x ) ) -> ( ( x oF - j ) e. D /\ ( x oF - j ) oR <_ x ) )
103 61 62 82 101 102 syl13anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( x oF - j ) e. D /\ ( x oF - j ) oR <_ x ) )
104 103 simpld 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( x oF - j ) e. D )
105 100 104 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( X ` ( x oF - j ) ) e. ( Base ` R ) )
106 26 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> Y : D --> ( Base ` R ) )
107 106 80 ffvelrnd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( Y ` j ) e. ( Base ` R ) )
108 10 37 crngcom 
 |-  ( ( R e. CRing /\ ( X ` ( x oF - j ) ) e. ( Base ` R ) /\ ( Y ` j ) e. ( Base ` R ) ) -> ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` j ) ) = ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) )
109 99 105 107 108 syl3anc 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` j ) ) = ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) )
110 98 109 eqtrd 
 |-  ( ( ( ph /\ x e. D ) /\ j e. { g e. D | g oR <_ x } ) -> ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` ( x oF - ( x oF - j ) ) ) ) = ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) )
111 110 mpteq2dva 
 |-  ( ( ph /\ x e. D ) -> ( j e. { g e. D | g oR <_ x } |-> ( ( X ` ( x oF - j ) ) ( .r ` R ) ( Y ` ( x oF - ( x oF - j ) ) ) ) ) = ( j e. { g e. D | g oR <_ x } |-> ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) ) )
112 72 111 eqtrd 
 |-  ( ( ph /\ x e. D ) -> ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) o. ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) ) = ( j e. { g e. D | g oR <_ x } |-> ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) ) )
113 112 oveq2d 
 |-  ( ( ph /\ x e. D ) -> ( R gsum ( ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) o. ( j e. { g e. D | g oR <_ x } |-> ( x oF - j ) ) ) ) = ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) ) ) )
114 60 113 eqtrd 
 |-  ( ( ph /\ x e. D ) -> ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) ) = ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) ) ) )
115 114 mpteq2dva 
 |-  ( ph -> ( x e. D |-> ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) ) ) = ( x e. D |-> ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) ) ) ) )
116 1 6 37 5 4 7 8 psrmulfval 
 |-  ( ph -> ( X .X. Y ) = ( x e. D |-> ( R gsum ( k e. { g e. D | g oR <_ x } |-> ( ( X ` k ) ( .r ` R ) ( Y ` ( x oF - k ) ) ) ) ) ) )
117 1 6 37 5 4 8 7 psrmulfval 
 |-  ( ph -> ( Y .X. X ) = ( x e. D |-> ( R gsum ( j e. { g e. D | g oR <_ x } |-> ( ( Y ` j ) ( .r ` R ) ( X ` ( x oF - j ) ) ) ) ) ) )
118 115 116 117 3eqtr4d 
 |-  ( ph -> ( X .X. Y ) = ( Y .X. X ) )