Metamath Proof Explorer

Theorem evlseu

Description: For a given interpretation of the variables G and of the scalars F , this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlseu.p 
|- P = ( I mPoly R )
evlseu.c 
|- C = ( Base ` S )
evlseu.a 
|- A = ( algSc ` P )
evlseu.v 
|- V = ( I mVar R )
evlseu.i 
|- ( ph -> I e. W )
evlseu.r 
|- ( ph -> R e. CRing )
evlseu.s 
|- ( ph -> S e. CRing )
evlseu.f 
|- ( ph -> F e. ( R RingHom S ) )
evlseu.g 
|- ( ph -> G : I --> C )
Assertion evlseu 
|- ( ph -> E! m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) )

Proof

Step Hyp Ref Expression
1 evlseu.p 
 |-  P = ( I mPoly R )
2 evlseu.c 
 |-  C = ( Base ` S )
3 evlseu.a 
 |-  A = ( algSc ` P )
4 evlseu.v 
 |-  V = ( I mVar R )
5 evlseu.i 
 |-  ( ph -> I e. W )
6 evlseu.r 
 |-  ( ph -> R e. CRing )
7 evlseu.s 
 |-  ( ph -> S e. CRing )
8 evlseu.f 
 |-  ( ph -> F e. ( R RingHom S ) )
9 evlseu.g 
 |-  ( ph -> G : I --> C )
10 eqid 
 |-  ( Base ` P ) = ( Base ` P )
11 eqid 
 |-  { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } = { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin }
12 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
13 eqid 
 |-  ( .g ` ( mulGrp ` S ) ) = ( .g ` ( mulGrp ` S ) )
14 eqid 
 |-  ( .r ` S ) = ( .r ` S )
15 eqid 
 |-  ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) = ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) )
16 1 10 2 11 12 13 14 4 15 5 6 7 8 9 3 evlslem1 
 |-  ( ph -> ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) e. ( P RingHom S ) /\ ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. A ) = F /\ ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. V ) = G ) )
17 coeq1 
 |-  ( m = ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) -> ( m o. A ) = ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. A ) )
18 17 eqeq1d 
 |-  ( m = ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) -> ( ( m o. A ) = F <-> ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. A ) = F ) )
19 coeq1 
 |-  ( m = ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) -> ( m o. V ) = ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. V ) )
20 19 eqeq1d 
 |-  ( m = ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) -> ( ( m o. V ) = G <-> ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. V ) = G ) )
21 18 20 anbi12d 
 |-  ( m = ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) -> ( ( ( m o. A ) = F /\ ( m o. V ) = G ) <-> ( ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. A ) = F /\ ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. V ) = G ) ) )
22 21 rspcev 
 |-  ( ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) e. ( P RingHom S ) /\ ( ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. A ) = F /\ ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. V ) = G ) ) -> E. m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) )
23 22 3impb 
 |-  ( ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) e. ( P RingHom S ) /\ ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. A ) = F /\ ( ( x e. ( Base ` P ) |-> ( S gsum ( y e. { z e. ( NN0 ^m I ) | ( `' z " NN ) e. Fin } |-> ( ( F ` ( x ` y ) ) ( .r ` S ) ( ( mulGrp ` S ) gsum ( y oF ( .g ` ( mulGrp ` S ) ) G ) ) ) ) ) ) o. V ) = G ) -> E. m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) )
24 16 23 syl 
 |-  ( ph -> E. m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) )
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 crngring 
 |-  ( R e. CRing -> R e. Ring )
27 6 26 syl 
 |-  ( ph -> R e. Ring )
28 1 10 25 3 5 27 mplasclf 
 |-  ( ph -> A : ( Base ` R ) --> ( Base ` P ) )
29 28 ffund 
 |-  ( ph -> Fun A )
30 funcoeqres 
 |-  ( ( Fun A /\ ( m o. A ) = F ) -> ( m |` ran A ) = ( F o. `' A ) )
31 29 30 sylan 
 |-  ( ( ph /\ ( m o. A ) = F ) -> ( m |` ran A ) = ( F o. `' A ) )
32 1 4 10 5 27 mvrf2 
 |-  ( ph -> V : I --> ( Base ` P ) )
33 32 ffund 
 |-  ( ph -> Fun V )
34 funcoeqres 
 |-  ( ( Fun V /\ ( m o. V ) = G ) -> ( m |` ran V ) = ( G o. `' V ) )
35 33 34 sylan 
 |-  ( ( ph /\ ( m o. V ) = G ) -> ( m |` ran V ) = ( G o. `' V ) )
36 31 35 anim12dan 
 |-  ( ( ph /\ ( ( m o. A ) = F /\ ( m o. V ) = G ) ) -> ( ( m |` ran A ) = ( F o. `' A ) /\ ( m |` ran V ) = ( G o. `' V ) ) )
37 36 ex 
 |-  ( ph -> ( ( ( m o. A ) = F /\ ( m o. V ) = G ) -> ( ( m |` ran A ) = ( F o. `' A ) /\ ( m |` ran V ) = ( G o. `' V ) ) ) )
38 resundi 
 |-  ( m |` ( ran A u. ran V ) ) = ( ( m |` ran A ) u. ( m |` ran V ) )
39 uneq12 
 |-  ( ( ( m |` ran A ) = ( F o. `' A ) /\ ( m |` ran V ) = ( G o. `' V ) ) -> ( ( m |` ran A ) u. ( m |` ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) )
40 38 39 syl5eq 
 |-  ( ( ( m |` ran A ) = ( F o. `' A ) /\ ( m |` ran V ) = ( G o. `' V ) ) -> ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) )
41 37 40 syl6 
 |-  ( ph -> ( ( ( m o. A ) = F /\ ( m o. V ) = G ) -> ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) )
42 41 ralrimivw 
 |-  ( ph -> A. m e. ( P RingHom S ) ( ( ( m o. A ) = F /\ ( m o. V ) = G ) -> ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) )
43 eqtr3 
 |-  ( ( ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) /\ ( n |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) -> ( m |` ( ran A u. ran V ) ) = ( n |` ( ran A u. ran V ) ) )
44 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
45 44 5 6 psrassa 
 |-  ( ph -> ( I mPwSer R ) e. AssAlg )
46 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
47 44 4 46 5 27 mvrf 
 |-  ( ph -> V : I --> ( Base ` ( I mPwSer R ) ) )
48 47 frnd 
 |-  ( ph -> ran V C_ ( Base ` ( I mPwSer R ) ) )
49 eqid 
 |-  ( AlgSpan ` ( I mPwSer R ) ) = ( AlgSpan ` ( I mPwSer R ) )
50 eqid 
 |-  ( algSc ` ( I mPwSer R ) ) = ( algSc ` ( I mPwSer R ) )
51 eqid 
 |-  ( mrCls ` ( SubRing ` ( I mPwSer R ) ) ) = ( mrCls ` ( SubRing ` ( I mPwSer R ) ) )
52 49 50 51 46 aspval2 
 |-  ( ( ( I mPwSer R ) e. AssAlg /\ ran V C_ ( Base ` ( I mPwSer R ) ) ) -> ( ( AlgSpan ` ( I mPwSer R ) ) ` ran V ) = ( ( mrCls ` ( SubRing ` ( I mPwSer R ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) )
53 45 48 52 syl2anc 
 |-  ( ph -> ( ( AlgSpan ` ( I mPwSer R ) ) ` ran V ) = ( ( mrCls ` ( SubRing ` ( I mPwSer R ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) )
54 1 44 4 49 5 6 mplbas2 
 |-  ( ph -> ( ( AlgSpan ` ( I mPwSer R ) ) ` ran V ) = ( Base ` P ) )
55 44 1 10 5 27 mplsubrg 
 |-  ( ph -> ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) )
56 1 44 10 mplval2 
 |-  P = ( ( I mPwSer R ) |`s ( Base ` P ) )
57 56 subsubrg2 
 |-  ( ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) -> ( SubRing ` P ) = ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) )
58 55 57 syl 
 |-  ( ph -> ( SubRing ` P ) = ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) )
59 58 fveq2d 
 |-  ( ph -> ( mrCls ` ( SubRing ` P ) ) = ( mrCls ` ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) ) )
60 50 56 ressascl 
 |-  ( ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) -> ( algSc ` ( I mPwSer R ) ) = ( algSc ` P ) )
61 55 60 syl 
 |-  ( ph -> ( algSc ` ( I mPwSer R ) ) = ( algSc ` P ) )
62 3 61 eqtr4id 
 |-  ( ph -> A = ( algSc ` ( I mPwSer R ) ) )
63 62 rneqd 
 |-  ( ph -> ran A = ran ( algSc ` ( I mPwSer R ) ) )
64 63 uneq1d 
 |-  ( ph -> ( ran A u. ran V ) = ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) )
65 59 64 fveq12d 
 |-  ( ph -> ( ( mrCls ` ( SubRing ` P ) ) ` ( ran A u. ran V ) ) = ( ( mrCls ` ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) )
66 assaring 
 |-  ( ( I mPwSer R ) e. AssAlg -> ( I mPwSer R ) e. Ring )
67 46 subrgmre 
 |-  ( ( I mPwSer R ) e. Ring -> ( SubRing ` ( I mPwSer R ) ) e. ( Moore ` ( Base ` ( I mPwSer R ) ) ) )
68 45 66 67 3syl 
 |-  ( ph -> ( SubRing ` ( I mPwSer R ) ) e. ( Moore ` ( Base ` ( I mPwSer R ) ) ) )
69 28 frnd 
 |-  ( ph -> ran A C_ ( Base ` P ) )
70 63 69 eqsstrrd 
 |-  ( ph -> ran ( algSc ` ( I mPwSer R ) ) C_ ( Base ` P ) )
71 32 frnd 
 |-  ( ph -> ran V C_ ( Base ` P ) )
72 70 71 unssd 
 |-  ( ph -> ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) C_ ( Base ` P ) )
73 eqid 
 |-  ( mrCls ` ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) ) = ( mrCls ` ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) )
74 51 73 submrc 
 |-  ( ( ( SubRing ` ( I mPwSer R ) ) e. ( Moore ` ( Base ` ( I mPwSer R ) ) ) /\ ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) /\ ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) C_ ( Base ` P ) ) -> ( ( mrCls ` ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) = ( ( mrCls ` ( SubRing ` ( I mPwSer R ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) )
75 68 55 72 74 syl3anc 
 |-  ( ph -> ( ( mrCls ` ( ( SubRing ` ( I mPwSer R ) ) i^i ~P ( Base ` P ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) = ( ( mrCls ` ( SubRing ` ( I mPwSer R ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) )
76 65 75 eqtr2d 
 |-  ( ph -> ( ( mrCls ` ( SubRing ` ( I mPwSer R ) ) ) ` ( ran ( algSc ` ( I mPwSer R ) ) u. ran V ) ) = ( ( mrCls ` ( SubRing ` P ) ) ` ( ran A u. ran V ) ) )
77 53 54 76 3eqtr3d 
 |-  ( ph -> ( Base ` P ) = ( ( mrCls ` ( SubRing ` P ) ) ` ( ran A u. ran V ) ) )
78 77 ad2antrr 
 |-  ( ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) /\ ( ran A u. ran V ) C_ dom ( m i^i n ) ) -> ( Base ` P ) = ( ( mrCls ` ( SubRing ` P ) ) ` ( ran A u. ran V ) ) )
79 1 mplring 
 |-  ( ( I e. W /\ R e. Ring ) -> P e. Ring )
80 5 27 79 syl2anc 
 |-  ( ph -> P e. Ring )
81 10 subrgmre 
 |-  ( P e. Ring -> ( SubRing ` P ) e. ( Moore ` ( Base ` P ) ) )
82 80 81 syl 
 |-  ( ph -> ( SubRing ` P ) e. ( Moore ` ( Base ` P ) ) )
83 82 ad2antrr 
 |-  ( ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) /\ ( ran A u. ran V ) C_ dom ( m i^i n ) ) -> ( SubRing ` P ) e. ( Moore ` ( Base ` P ) ) )
84 simpr 
 |-  ( ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) /\ ( ran A u. ran V ) C_ dom ( m i^i n ) ) -> ( ran A u. ran V ) C_ dom ( m i^i n ) )
85 rhmeql 
 |-  ( ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) -> dom ( m i^i n ) e. ( SubRing ` P ) )
86 85 ad2antlr 
 |-  ( ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) /\ ( ran A u. ran V ) C_ dom ( m i^i n ) ) -> dom ( m i^i n ) e. ( SubRing ` P ) )
87 eqid 
 |-  ( mrCls ` ( SubRing ` P ) ) = ( mrCls ` ( SubRing ` P ) )
88 87 mrcsscl 
 |-  ( ( ( SubRing ` P ) e. ( Moore ` ( Base ` P ) ) /\ ( ran A u. ran V ) C_ dom ( m i^i n ) /\ dom ( m i^i n ) e. ( SubRing ` P ) ) -> ( ( mrCls ` ( SubRing ` P ) ) ` ( ran A u. ran V ) ) C_ dom ( m i^i n ) )
89 83 84 86 88 syl3anc 
 |-  ( ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) /\ ( ran A u. ran V ) C_ dom ( m i^i n ) ) -> ( ( mrCls ` ( SubRing ` P ) ) ` ( ran A u. ran V ) ) C_ dom ( m i^i n ) )
90 78 89 eqsstrd 
 |-  ( ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) /\ ( ran A u. ran V ) C_ dom ( m i^i n ) ) -> ( Base ` P ) C_ dom ( m i^i n ) )
91 90 ex 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ( ( ran A u. ran V ) C_ dom ( m i^i n ) -> ( Base ` P ) C_ dom ( m i^i n ) ) )
92 simprl 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> m e. ( P RingHom S ) )
93 10 2 rhmf 
 |-  ( m e. ( P RingHom S ) -> m : ( Base ` P ) --> C )
94 ffn 
 |-  ( m : ( Base ` P ) --> C -> m Fn ( Base ` P ) )
95 92 93 94 3syl 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> m Fn ( Base ` P ) )
96 simprr 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> n e. ( P RingHom S ) )
97 10 2 rhmf 
 |-  ( n e. ( P RingHom S ) -> n : ( Base ` P ) --> C )
98 ffn 
 |-  ( n : ( Base ` P ) --> C -> n Fn ( Base ` P ) )
99 96 97 98 3syl 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> n Fn ( Base ` P ) )
100 69 adantr 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ran A C_ ( Base ` P ) )
101 71 adantr 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ran V C_ ( Base ` P ) )
102 100 101 unssd 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ( ran A u. ran V ) C_ ( Base ` P ) )
103 fnreseql 
 |-  ( ( m Fn ( Base ` P ) /\ n Fn ( Base ` P ) /\ ( ran A u. ran V ) C_ ( Base ` P ) ) -> ( ( m |` ( ran A u. ran V ) ) = ( n |` ( ran A u. ran V ) ) <-> ( ran A u. ran V ) C_ dom ( m i^i n ) ) )
104 95 99 102 103 syl3anc 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ( ( m |` ( ran A u. ran V ) ) = ( n |` ( ran A u. ran V ) ) <-> ( ran A u. ran V ) C_ dom ( m i^i n ) ) )
105 fneqeql2 
 |-  ( ( m Fn ( Base ` P ) /\ n Fn ( Base ` P ) ) -> ( m = n <-> ( Base ` P ) C_ dom ( m i^i n ) ) )
106 95 99 105 syl2anc 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ( m = n <-> ( Base ` P ) C_ dom ( m i^i n ) ) )
107 91 104 106 3imtr4d 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ( ( m |` ( ran A u. ran V ) ) = ( n |` ( ran A u. ran V ) ) -> m = n ) )
108 43 107 syl5 
 |-  ( ( ph /\ ( m e. ( P RingHom S ) /\ n e. ( P RingHom S ) ) ) -> ( ( ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) /\ ( n |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) -> m = n ) )
109 108 ralrimivva 
 |-  ( ph -> A. m e. ( P RingHom S ) A. n e. ( P RingHom S ) ( ( ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) /\ ( n |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) -> m = n ) )
110 reseq1 
 |-  ( m = n -> ( m |` ( ran A u. ran V ) ) = ( n |` ( ran A u. ran V ) ) )
111 110 eqeq1d 
 |-  ( m = n -> ( ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) <-> ( n |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) )
112 111 rmo4 
 |-  ( E* m e. ( P RingHom S ) ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) <-> A. m e. ( P RingHom S ) A. n e. ( P RingHom S ) ( ( ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) /\ ( n |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) -> m = n ) )
113 109 112 sylibr 
 |-  ( ph -> E* m e. ( P RingHom S ) ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) )
114 rmoim 
 |-  ( A. m e. ( P RingHom S ) ( ( ( m o. A ) = F /\ ( m o. V ) = G ) -> ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) ) -> ( E* m e. ( P RingHom S ) ( m |` ( ran A u. ran V ) ) = ( ( F o. `' A ) u. ( G o. `' V ) ) -> E* m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) ) )
115 42 113 114 sylc 
 |-  ( ph -> E* m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) )
116 reu5 
 |-  ( E! m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) <-> ( E. m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) /\ E* m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) ) )
117 24 115 116 sylanbrc 
 |-  ( ph -> E! m e. ( P RingHom S ) ( ( m o. A ) = F /\ ( m o. V ) = G ) )