Metamath Proof Explorer


Theorem selvcl

Description: Closure of the "variable selection" function. (Contributed by SN, 22-Feb-2024)

Ref Expression
Hypotheses selvcl.p P=ImPolyR
selvcl.b B=BaseP
selvcl.u U=IJmPolyR
selvcl.t T=JmPolyU
selvcl.e E=BaseT
selvcl.i φIV
selvcl.r φRCRing
selvcl.j φJI
selvcl.f φFB
Assertion selvcl φIselectVarsRJFE

Proof

Step Hyp Ref Expression
1 selvcl.p P=ImPolyR
2 selvcl.b B=BaseP
3 selvcl.u U=IJmPolyR
4 selvcl.t T=JmPolyU
5 selvcl.e E=BaseT
6 selvcl.i φIV
7 selvcl.r φRCRing
8 selvcl.j φJI
9 selvcl.f φFB
10 eqid algScT=algScT
11 eqid algScTalgScU=algScTalgScU
12 1 2 3 4 10 11 6 7 8 9 selvval φIselectVarsRJF=IevalSubTranalgScTalgScUalgScTalgScUFxIifxJJmVarUxalgScTIJmVarRx
13 eqid T𝑠EI=T𝑠EI
14 eqid BaseT𝑠EI=BaseT𝑠EI
15 6 8 ssexd φJV
16 6 difexd φIJV
17 3 mplcrng IJVRCRingUCRing
18 16 7 17 syl2anc φUCRing
19 4 mplcrng JVUCRingTCRing
20 15 18 19 syl2anc φTCRing
21 ovexd φEIV
22 eqid IevalSubTranalgScTalgScU=IevalSubTranalgScTalgScU
23 eqid ImPolyT𝑠ranalgScTalgScU=ImPolyT𝑠ranalgScTalgScU
24 eqid T𝑠ranalgScTalgScU=T𝑠ranalgScTalgScU
25 3 4 10 11 22 23 24 13 5 6 7 8 selvval2lemn φIevalSubTranalgScTalgScUImPolyT𝑠ranalgScTalgScURingHomT𝑠EI
26 eqid BaseImPolyT𝑠ranalgScTalgScU=BaseImPolyT𝑠ranalgScTalgScU
27 26 14 rhmf IevalSubTranalgScTalgScUImPolyT𝑠ranalgScTalgScURingHomT𝑠EIIevalSubTranalgScTalgScU:BaseImPolyT𝑠ranalgScTalgScUBaseT𝑠EI
28 25 27 syl φIevalSubTranalgScTalgScU:BaseImPolyT𝑠ranalgScTalgScUBaseT𝑠EI
29 1 2 3 4 10 11 24 23 26 6 7 8 9 selvval2lem4 φalgScTalgScUFBaseImPolyT𝑠ranalgScTalgScU
30 28 29 ffvelrnd φIevalSubTranalgScTalgScUalgScTalgScUFBaseT𝑠EI
31 13 5 14 20 21 30 pwselbas φIevalSubTranalgScTalgScUalgScTalgScUF:EIE
32 eqid xIifxJJmVarUxalgScTIJmVarRx=xIifxJJmVarUxalgScTIJmVarRx
33 3 4 10 5 32 6 7 8 selvval2lem5 φxIifxJJmVarUxalgScTIJmVarRxEI
34 31 33 ffvelrnd φIevalSubTranalgScTalgScUalgScTalgScUFxIifxJJmVarUxalgScTIJmVarRxE
35 12 34 eqeltrd φIselectVarsRJFE