Metamath Proof Explorer

Theorem 0mplrim

Description: Build a ring isomorphism between multivariate polynomials with no variables and the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses 0mplric.b 
|- B = ( Base ` P )
0mplric.p 
|- P = ( (/) mPoly R )
0mplric.r 
|- ( ph -> R e. Ring )
0mplrim.f 
|- F = ( p e. B |-> ( p ` (/) ) )
Assertion 0mplrim 
|- ( ph -> F e. ( P RingIso R ) )

Proof

Step Hyp Ref Expression
1 0mplric.b 
 |-  B = ( Base ` P )
2 0mplric.p 
 |-  P = ( (/) mPoly R )
3 0mplric.r 
 |-  ( ph -> R e. Ring )
4 0mplrim.f 
 |-  F = ( p e. B |-> ( p ` (/) ) )
5 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
6 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 eqid 
 |-  ( .r ` P ) = ( .r ` P )
8 eqid 
 |-  ( .r ` R ) = ( .r ` R )
9 0ex 
 |-  (/) e. _V
10 9 a1i 
 |-  ( ph -> (/) e. _V )
11 2 10 3 mplringd 
 |-  ( ph -> P e. Ring )
12 fveq1 
 |-  ( p = ( 1r ` P ) -> ( p ` (/) ) = ( ( 1r ` P ) ` (/) ) )
13 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
14 2 13 6 5 10 3 mplascl1 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
15 14 fveq1d 
 |-  ( ph -> ( ( ( algSc ` P ) ` ( 1r ` R ) ) ` (/) ) = ( ( 1r ` P ) ` (/) ) )
16 eqid 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } = { h e. ( NN0 ^m (/) ) | h finSupp 0 }
17 16 psrbasfsupp 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } = { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin }
18 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
19 eqid 
 |-  ( Base ` R ) = ( Base ` R )
20 19 6 3 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
21 2 17 18 19 13 10 3 20 mplascl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( p e. { h e. ( NN0 ^m (/) ) | h finSupp 0 } |-> if ( p = ( (/) X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
22 simpr 
 |-  ( ( ph /\ p = (/) ) -> p = (/) )
23 0xp 
 |-  ( (/) X. { 0 } ) = (/)
24 22 23 eqtr4di 
 |-  ( ( ph /\ p = (/) ) -> p = ( (/) X. { 0 } ) )
25 24 iftrued 
 |-  ( ( ph /\ p = (/) ) -> if ( p = ( (/) X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
26 breq1 
 |-  ( h = (/) -> ( h finSupp 0 <-> (/) finSupp 0 ) )
27 nn0ex 
 |-  NN0 e. _V
28 27 a1i 
 |-  ( T. -> NN0 e. _V )
29 9 a1i 
 |-  ( T. -> (/) e. _V )
30 f0 
 |-  (/) : (/) --> NN0
31 30 a1i 
 |-  ( T. -> (/) : (/) --> NN0 )
32 28 29 31 elmapdd 
 |-  ( T. -> (/) e. ( NN0 ^m (/) ) )
33 0fi 
 |-  (/) e. Fin
34 33 a1i 
 |-  ( T. -> (/) e. Fin )
35 c0ex 
 |-  0 e. _V
36 35 a1i 
 |-  ( T. -> 0 e. _V )
37 31 34 36 fidmfisupp 
 |-  ( T. -> (/) finSupp 0 )
38 26 32 37 elrabd 
 |-  ( T. -> (/) e. { h e. ( NN0 ^m (/) ) | h finSupp 0 } )
39 38 mptru 
 |-  (/) e. { h e. ( NN0 ^m (/) ) | h finSupp 0 }
40 39 a1i 
 |-  ( ph -> (/) e. { h e. ( NN0 ^m (/) ) | h finSupp 0 } )
41 21 25 40 20 fvmptd 
 |-  ( ph -> ( ( ( algSc ` P ) ` ( 1r ` R ) ) ` (/) ) = ( 1r ` R ) )
42 15 41 eqtr3d 
 |-  ( ph -> ( ( 1r ` P ) ` (/) ) = ( 1r ` R ) )
43 12 42 sylan9eqr 
 |-  ( ( ph /\ p = ( 1r ` P ) ) -> ( p ` (/) ) = ( 1r ` R ) )
44 1 5 11 ringidcld 
 |-  ( ph -> ( 1r ` P ) e. B )
45 4 43 44 20 fvmptd2 
 |-  ( ph -> ( F ` ( 1r ` P ) ) = ( 1r ` R ) )
46 fveq1 
 |-  ( p = ( x ( .r ` P ) y ) -> ( p ` (/) ) = ( ( x ( .r ` P ) y ) ` (/) ) )
47 11 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> P e. Ring )
48 simplr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> x e. B )
49 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> y e. B )
50 1 7 47 48 49 ringcld 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x ( .r ` P ) y ) e. B )
51 fvexd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( x ( .r ` P ) y ) ` (/) ) e. _V )
52 4 46 50 51 fvmptd3 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( F ` ( x ( .r ` P ) y ) ) = ( ( x ( .r ` P ) y ) ` (/) ) )
53 elsni 
 |-  ( p e. { (/) } -> p = (/) )
54 39 a1i 
 |-  ( p e. { (/) } -> (/) e. { h e. ( NN0 ^m (/) ) | h finSupp 0 } )
55 53 54 eqeltrd 
 |-  ( p e. { (/) } -> p e. { h e. ( NN0 ^m (/) ) | h finSupp 0 } )
56 ssrab2 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } C_ ( NN0 ^m (/) )
57 mapdm0 
 |-  ( NN0 e. _V -> ( NN0 ^m (/) ) = { (/) } )
58 27 57 ax-mp 
 |-  ( NN0 ^m (/) ) = { (/) }
59 56 58 sseqtri 
 |-  { h e. ( NN0 ^m (/) ) | h finSupp 0 } C_ { (/) }
60 59 sseli 
 |-  ( p e. { h e. ( NN0 ^m (/) ) | h finSupp 0 } -> p e. { (/) } )
61 55 60 impbii 
 |-  ( p e. { (/) } <-> p e. { h e. ( NN0 ^m (/) ) | h finSupp 0 } )
62 61 eqriv 
 |-  { (/) } = { h e. ( NN0 ^m (/) ) | h finSupp 0 }
63 62 psrbasfsupp 
 |-  { (/) } = { h e. ( NN0 ^m (/) ) | ( `' h " NN ) e. Fin }
64 2 1 8 7 63 48 49 mplmul 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x ( .r ` P ) y ) = ( p e. { (/) } |-> ( R gsum ( q e. { r e. { (/) } | r oR <_ p } |-> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) ) ) ) )
65 3 ringgrpd 
 |-  ( ph -> R e. Grp )
66 65 grpmndd 
 |-  ( ph -> R e. Mnd )
67 66 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> R e. Mnd )
68 9 a1i 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> (/) e. _V )
69 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> R e. Ring )
70 2 19 1 63 48 mplelf 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> x : { (/) } --> ( Base ` R ) )
71 70 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> x : { (/) } --> ( Base ` R ) )
72 9 snid 
 |-  (/) e. { (/) }
73 72 a1i 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> (/) e. { (/) } )
74 71 73 ffvelcdmd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( x ` (/) ) e. ( Base ` R ) )
75 2 19 1 63 49 mplelf 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> y : { (/) } --> ( Base ` R ) )
76 75 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> y : { (/) } --> ( Base ` R ) )
77 76 73 ffvelcdmd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( y ` (/) ) e. ( Base ` R ) )
78 19 8 69 74 77 ringcld 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( ( x ` (/) ) ( .r ` R ) ( y ` (/) ) ) e. ( Base ` R ) )
79 simpr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> q = (/) )
80 79 fveq2d 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> ( x ` q ) = ( x ` (/) ) )
81 9 a1i 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> (/) e. _V )
82 simplr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> p = (/) )
83 82 eqcomd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> (/) = p )
84 30 a1i 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> (/) : (/) --> NN0 )
85 83 84 feq1dd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> p : (/) --> NN0 )
86 85 ffnd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> p Fn (/) )
87 79 eqcomd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> (/) = q )
88 87 84 feq1dd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> q : (/) --> NN0 )
89 88 ffnd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> q Fn (/) )
90 81 86 89 offvalfv 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> ( p oF - q ) = ( a e. (/) |-> ( ( p ` a ) - ( q ` a ) ) ) )
91 mpt0 
 |-  ( a e. (/) |-> ( ( p ` a ) - ( q ` a ) ) ) = (/)
92 90 91 eqtrdi 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> ( p oF - q ) = (/) )
93 92 fveq2d 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> ( y ` ( p oF - q ) ) = ( y ` (/) ) )
94 80 93 oveq12d 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ q = (/) ) -> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) = ( ( x ` (/) ) ( .r ` R ) ( y ` (/) ) ) )
95 19 67 68 78 94 gsumsnd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( R gsum ( q e. { (/) } |-> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) ) ) = ( ( x ` (/) ) ( .r ` R ) ( y ` (/) ) ) )
96 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) /\ a e. (/) ) -> a e. (/) )
97 noel 
 |-  -. a e. (/)
98 97 a1i 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) /\ a e. (/) ) -> -. a e. (/) )
99 96 98 pm2.21dd 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) /\ a e. (/) ) -> ( r ` a ) <_ ( p ` a ) )
100 99 ralrimiva 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> A. a e. (/) ( r ` a ) <_ ( p ` a ) )
101 simpr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> r e. { (/) } )
102 101 elsnd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> r = (/) )
103 102 eqcomd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> (/) = r )
104 30 a1i 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> (/) : (/) --> NN0 )
105 103 104 feq1dd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> r : (/) --> NN0 )
106 105 ffnd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> r Fn (/) )
107 simplr 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> p = (/) )
108 107 eqcomd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> (/) = p )
109 108 104 feq1dd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> p : (/) --> NN0 )
110 109 ffnd 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> p Fn (/) )
111 vex 
 |-  p e. _V
112 111 a1i 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> p e. _V )
113 inidm 
 |-  ( (/) i^i (/) ) = (/)
114 eqidd 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) /\ a e. (/) ) -> ( r ` a ) = ( r ` a ) )
115 eqidd 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) /\ a e. (/) ) -> ( p ` a ) = ( p ` a ) )
116 106 110 101 112 113 114 115 ofrfvalg 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> ( r oR <_ p <-> A. a e. (/) ( r ` a ) <_ ( p ` a ) ) )
117 100 116 mpbird 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) /\ r e. { (/) } ) -> r oR <_ p )
118 117 rabeqcda 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> { r e. { (/) } | r oR <_ p } = { (/) } )
119 118 mpteq1d 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( q e. { r e. { (/) } | r oR <_ p } |-> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) ) = ( q e. { (/) } |-> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) ) )
120 119 oveq2d 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( R gsum ( q e. { r e. { (/) } | r oR <_ p } |-> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) ) ) = ( R gsum ( q e. { (/) } |-> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) ) ) )
121 fveq1 
 |-  ( p = x -> ( p ` (/) ) = ( x ` (/) ) )
122 fvexd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x ` (/) ) e. _V )
123 4 121 48 122 fvmptd3 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( F ` x ) = ( x ` (/) ) )
124 123 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( F ` x ) = ( x ` (/) ) )
125 fveq1 
 |-  ( p = y -> ( p ` (/) ) = ( y ` (/) ) )
126 fvexd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( y ` (/) ) e. _V )
127 4 125 49 126 fvmptd3 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( F ` y ) = ( y ` (/) ) )
128 127 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( F ` y ) = ( y ` (/) ) )
129 124 128 oveq12d 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( ( F ` x ) ( .r ` R ) ( F ` y ) ) = ( ( x ` (/) ) ( .r ` R ) ( y ` (/) ) ) )
130 95 120 129 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = (/) ) -> ( R gsum ( q e. { r e. { (/) } | r oR <_ p } |-> ( ( x ` q ) ( .r ` R ) ( y ` ( p oF - q ) ) ) ) ) = ( ( F ` x ) ( .r ` R ) ( F ` y ) ) )
131 72 a1i 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> (/) e. { (/) } )
132 ovexd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( F ` x ) ( .r ` R ) ( F ` y ) ) e. _V )
133 64 130 131 132 fvmptd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( x ( .r ` P ) y ) ` (/) ) = ( ( F ` x ) ( .r ` R ) ( F ` y ) ) )
134 52 133 eqtrd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( F ` ( x ( .r ` P ) y ) ) = ( ( F ` x ) ( .r ` R ) ( F ` y ) ) )
135 134 anasss 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x ( .r ` P ) y ) ) = ( ( F ` x ) ( .r ` R ) ( F ` y ) ) )
136 eqid 
 |-  ( +g ` P ) = ( +g ` P )
137 eqid 
 |-  ( +g ` R ) = ( +g ` R )
138 fvexd 
 |-  ( ( ph /\ p e. B ) -> ( p ` (/) ) e. _V )
139 snex 
 |-  { <. (/) , a >. } e. _V
140 139 a1i 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> { <. (/) , a >. } e. _V )
141 simpr 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> a = ( p ` (/) ) )
142 simplr 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> p e. B )
143 2 19 1 63 142 mplelf 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> p : { (/) } --> ( Base ` R ) )
144 72 a1i 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> (/) e. { (/) } )
145 143 144 ffvelcdmd 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> ( p ` (/) ) e. ( Base ` R ) )
146 141 145 eqeltrd 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> a e. ( Base ` R ) )
147 146 elexd 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> a e. _V )
148 fvsng 
 |-  ( ( (/) e. _V /\ a e. _V ) -> ( { <. (/) , a >. } ` (/) ) = a )
149 9 147 148 sylancr 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> ( { <. (/) , a >. } ` (/) ) = a )
150 149 141 eqtr2d 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> ( p ` (/) ) = ( { <. (/) , a >. } ` (/) ) )
151 9 a1i 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> (/) e. _V )
152 eqid 
 |-  { (/) } = { (/) }
153 143 ffnd 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> p Fn { (/) } )
154 151 147 fsnd 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> { <. (/) , a >. } : { (/) } --> _V )
155 154 ffnd 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> { <. (/) , a >. } Fn { (/) } )
156 151 152 153 155 fsneq 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> ( p = { <. (/) , a >. } <-> ( p ` (/) ) = ( { <. (/) , a >. } ` (/) ) ) )
157 150 156 mpbird 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> p = { <. (/) , a >. } )
158 146 157 jca 
 |-  ( ( ( ph /\ p e. B ) /\ a = ( p ` (/) ) ) -> ( a e. ( Base ` R ) /\ p = { <. (/) , a >. } ) )
159 158 anasss 
 |-  ( ( ph /\ ( p e. B /\ a = ( p ` (/) ) ) ) -> ( a e. ( Base ` R ) /\ p = { <. (/) , a >. } ) )
160 simpr 
 |-  ( ( ( ph /\ a e. ( Base ` R ) ) /\ p = { <. (/) , a >. } ) -> p = { <. (/) , a >. } )
161 fvexd 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> ( Base ` R ) e. _V )
162 snex 
 |-  { (/) } e. _V
163 162 a1i 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> { (/) } e. _V )
164 9 a1i 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> (/) e. _V )
165 simpr 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> a e. ( Base ` R ) )
166 164 165 fsnd 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> { <. (/) , a >. } : { (/) } --> ( Base ` R ) )
167 161 163 166 elmapdd 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> { <. (/) , a >. } e. ( ( Base ` R ) ^m { (/) } ) )
168 eqid 
 |-  ( (/) mPwSer R ) = ( (/) mPwSer R )
169 eqid 
 |-  ( Base ` ( (/) mPwSer R ) ) = ( Base ` ( (/) mPwSer R ) )
170 168 19 63 169 164 psrbas 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> ( Base ` ( (/) mPwSer R ) ) = ( ( Base ` R ) ^m { (/) } ) )
171 167 170 eleqtrrd 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> { <. (/) , a >. } e. ( Base ` ( (/) mPwSer R ) ) )
172 fvexd 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> ( 0g ` R ) e. _V )
173 snopfsupp 
 |-  ( ( (/) e. _V /\ a e. ( Base ` R ) /\ ( 0g ` R ) e. _V ) -> { <. (/) , a >. } finSupp ( 0g ` R ) )
174 9 165 172 173 mp3an2i 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> { <. (/) , a >. } finSupp ( 0g ` R ) )
175 2 168 169 18 1 mplelbas 
 |-  ( { <. (/) , a >. } e. B <-> ( { <. (/) , a >. } e. ( Base ` ( (/) mPwSer R ) ) /\ { <. (/) , a >. } finSupp ( 0g ` R ) ) )
176 171 174 175 sylanbrc 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> { <. (/) , a >. } e. B )
177 176 adantr 
 |-  ( ( ( ph /\ a e. ( Base ` R ) ) /\ p = { <. (/) , a >. } ) -> { <. (/) , a >. } e. B )
178 160 177 eqeltrd 
 |-  ( ( ( ph /\ a e. ( Base ` R ) ) /\ p = { <. (/) , a >. } ) -> p e. B )
179 160 fveq1d 
 |-  ( ( ( ph /\ a e. ( Base ` R ) ) /\ p = { <. (/) , a >. } ) -> ( p ` (/) ) = ( { <. (/) , a >. } ` (/) ) )
180 fvsng 
 |-  ( ( (/) e. _V /\ a e. ( Base ` R ) ) -> ( { <. (/) , a >. } ` (/) ) = a )
181 9 165 180 sylancr 
 |-  ( ( ph /\ a e. ( Base ` R ) ) -> ( { <. (/) , a >. } ` (/) ) = a )
182 181 adantr 
 |-  ( ( ( ph /\ a e. ( Base ` R ) ) /\ p = { <. (/) , a >. } ) -> ( { <. (/) , a >. } ` (/) ) = a )
183 179 182 eqtr2d 
 |-  ( ( ( ph /\ a e. ( Base ` R ) ) /\ p = { <. (/) , a >. } ) -> a = ( p ` (/) ) )
184 178 183 jca 
 |-  ( ( ( ph /\ a e. ( Base ` R ) ) /\ p = { <. (/) , a >. } ) -> ( p e. B /\ a = ( p ` (/) ) ) )
185 184 anasss 
 |-  ( ( ph /\ ( a e. ( Base ` R ) /\ p = { <. (/) , a >. } ) ) -> ( p e. B /\ a = ( p ` (/) ) ) )
186 159 185 impbida 
 |-  ( ph -> ( ( p e. B /\ a = ( p ` (/) ) ) <-> ( a e. ( Base ` R ) /\ p = { <. (/) , a >. } ) ) )
187 4 138 140 186 f1od 
 |-  ( ph -> F : B -1-1-onto-> ( Base ` R ) )
188 f1of 
 |-  ( F : B -1-1-onto-> ( Base ` R ) -> F : B --> ( Base ` R ) )
189 187 188 syl 
 |-  ( ph -> F : B --> ( Base ` R ) )
190 simpr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> p = ( x ( +g ` P ) y ) )
191 190 fveq1d 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> ( p ` (/) ) = ( ( x ( +g ` P ) y ) ` (/) ) )
192 simpllr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> x e. B )
193 simplr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> y e. B )
194 2 1 137 136 192 193 mpladd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> ( x ( +g ` P ) y ) = ( x oF ( +g ` R ) y ) )
195 194 fveq1d 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> ( ( x ( +g ` P ) y ) ` (/) ) = ( ( x oF ( +g ` R ) y ) ` (/) ) )
196 70 ffnd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> x Fn { (/) } )
197 75 ffnd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> y Fn { (/) } )
198 162 a1i 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> { (/) } e. _V )
199 inidm 
 |-  ( { (/) } i^i { (/) } ) = { (/) }
200 eqidd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ (/) e. { (/) } ) -> ( x ` (/) ) = ( x ` (/) ) )
201 eqidd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ (/) e. { (/) } ) -> ( y ` (/) ) = ( y ` (/) ) )
202 196 197 198 198 199 200 201 ofval 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ (/) e. { (/) } ) -> ( ( x oF ( +g ` R ) y ) ` (/) ) = ( ( x ` (/) ) ( +g ` R ) ( y ` (/) ) ) )
203 72 202 mpan2 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( x oF ( +g ` R ) y ) ` (/) ) = ( ( x ` (/) ) ( +g ` R ) ( y ` (/) ) ) )
204 203 adantr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> ( ( x oF ( +g ` R ) y ) ` (/) ) = ( ( x ` (/) ) ( +g ` R ) ( y ` (/) ) ) )
205 191 195 204 3eqtrd 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. B ) /\ p = ( x ( +g ` P ) y ) ) -> ( p ` (/) ) = ( ( x ` (/) ) ( +g ` R ) ( y ` (/) ) ) )
206 11 ringgrpd 
 |-  ( ph -> P e. Grp )
207 206 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> P e. Grp )
208 1 136 207 48 49 grpcld 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( x ( +g ` P ) y ) e. B )
209 ovexd 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( x ` (/) ) ( +g ` R ) ( y ` (/) ) ) e. _V )
210 4 205 208 209 fvmptd2 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( F ` ( x ( +g ` P ) y ) ) = ( ( x ` (/) ) ( +g ` R ) ( y ` (/) ) ) )
211 123 127 oveq12d 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( F ` x ) ( +g ` R ) ( F ` y ) ) = ( ( x ` (/) ) ( +g ` R ) ( y ` (/) ) ) )
212 210 211 eqtr4d 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( F ` ( x ( +g ` P ) y ) ) = ( ( F ` x ) ( +g ` R ) ( F ` y ) ) )
213 212 anasss 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x ( +g ` P ) y ) ) = ( ( F ` x ) ( +g ` R ) ( F ` y ) ) )
214 1 5 6 7 8 11 3 45 135 19 136 137 189 213 isrhmd 
 |-  ( ph -> F e. ( P RingHom R ) )
215 1 19 isrim 
 |-  ( F e. ( P RingIso R ) <-> ( F e. ( P RingHom R ) /\ F : B -1-1-onto-> ( Base ` R ) ) )
216 214 187 215 sylanbrc 
 |-  ( ph -> F e. ( P RingIso R ) )