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\mathrm{mPoly}R$$
	evlseu.c	$$⊢C={\mathrm{Base}}_S$$
	evlseu.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	evlseu.v	$$⊢V=I\mathrm{mVar}R$$
	evlseu.i	$$⊢\phi \to I\in W$$
	evlseu.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	evlseu.s	$$⊢\phi \to S\in \mathrm{CRing}$$
	evlseu.f	$$⊢\phi \to F\in \left(R\mathrm{RingHom}S\right)$$
	evlseu.g	$$⊢\phi \to G:I⟶C$$
Assertion	evlseu	$$⊢\phi \to \exists !m\in \left(P\mathrm{RingHom}S\right)\left(m\circ A=F\wedge m\circ V=G\right)$$

Proof

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