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