Theorem mplasclco

Description: Case where composing an algebra scalar lifting functions with a scalar leads to a scalar. This is useful when working with selectVars . (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	mplasclco.s	$$⊢S={\mathrm{Base}}_R$$
	mplasclco.o	$$⊢O=J\mathrm{mPoly}R$$
	mplasclco.p	$$⊢P=I\mathrm{mPoly}R$$
	mplasclco.q	$$⊢Q=I\mathrm{mPoly}O$$
	mplasclco.a	$$⊢A=\mathrm{algSc}\left(O\right)$$
	mplasclco.b	$$⊢B=\mathrm{algSc}\left(P\right)$$
	mplasclco.c	$$⊢C=\mathrm{algSc}\left(Q\right)$$
	mplasclco.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplasclco.e	$$⊢E=\left\{j\in \left({{\mathbb{N}}_0}^J\right)|j^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mplasclco.i	$$⊢\phi \to I\in V$$
	mplasclco.j	$$⊢\phi \to J\subseteq I$$
	mplasclco.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	mplasclco.x	$$⊢\phi \to X\in S$$
Assertion	mplasclco	$$⊢\phi \to A\circ B\left(X\right)=C\left(A\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplasclco.s	$$⊢S={\mathrm{Base}}_R$$
2		mplasclco.o	$$⊢O=J\mathrm{mPoly}R$$
3		mplasclco.p	$$⊢P=I\mathrm{mPoly}R$$
4		mplasclco.q	$$⊢Q=I\mathrm{mPoly}O$$
5		mplasclco.a	$$⊢A=\mathrm{algSc}\left(O\right)$$
6		mplasclco.b	$$⊢B=\mathrm{algSc}\left(P\right)$$
7		mplasclco.c	$$⊢C=\mathrm{algSc}\left(Q\right)$$
8		mplasclco.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
9		mplasclco.e	$$⊢E=\left\{j\in \left({{\mathbb{N}}_0}^J\right)|j^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
10		mplasclco.i	$$⊢\phi \to I\in V$$
11		mplasclco.j	$$⊢\phi \to J\subseteq I$$
12		mplasclco.r	$$⊢\phi \to R\in \mathrm{CRing}$$
13		mplasclco.x	$$⊢\phi \to X\in S$$
14		eqid	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_O$$
15	10 11	ssexd	$$⊢\phi \to J\in \mathrm{V}$$
16	12	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
17	2 14 1 5 15 16	mplasclf	$$⊢\phi \to A:S⟶{\mathrm{Base}}_O$$
18		eqid	$$⊢0_R=0_R$$
19	3 8 18 1 6 10 16 13	mplascl	$$⊢\phi \to B\left(X\right)=\left(n\in D⟼if\left(n=I\times \left\{0\right\},X,0_R\right)\right)$$
20	12	crnggrpd	$$⊢\phi \to R\in \mathrm{Grp}$$
21	1 18 20	grpidcld	$$⊢\phi \to 0_R\in S$$
22	13 21	ifcld	$$⊢\phi \to if\left(n=I\times \left\{0\right\},X,0_R\right)\in S$$
23	22	adantr	$$⊢\left(\phi \wedge n\in D\right)\to if\left(n=I\times \left\{0\right\},X,0_R\right)\in S$$
24	19 23	fmpt3d	$$⊢\phi \to B\left(X\right):D⟶S$$
25	17 24	fcod	$$⊢\phi \to \left(A\circ B\left(X\right)\right):D⟶{\mathrm{Base}}_O$$
26	25	ffnd	$$⊢\phi \to \left(A\circ B\left(X\right)\right)FnD$$
27		eqid	$$⊢0_O=0_O$$
28	2 15 16	mplringd	$$⊢\phi \to O\in \mathrm{Ring}$$
29		eqid	$$⊢\mathrm{Scalar}\left(O\right)=\mathrm{Scalar}\left(O\right)$$
30		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(O\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(O\right)}$$
31	2	mplassa	$$⊢\left(J\in \mathrm{V}\wedge R\in \mathrm{CRing}\right)\to O\in \mathrm{AssAlg}$$
32	15 12 31	syl2anc	$$⊢\phi \to O\in \mathrm{AssAlg}$$
33	2 15 12	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(O\right)$$
34	33	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(O\right)}$$
35	1 34	eqtrid	$$⊢\phi \to S={\mathrm{Base}}_{\mathrm{Scalar}\left(O\right)}$$
36	13 35	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(O\right)}$$
37	5 29 30 32 36	asclelbas	$$⊢\phi \to A\left(X\right)\in {\mathrm{Base}}_O$$
38	4 8 27 14 7 10 28 37	mplascl	$$⊢\phi \to C\left(A\left(X\right)\right)=\left(n\in D⟼if\left(n=I\times \left\{0\right\},A\left(X\right),0_O\right)\right)$$
39	28	ringgrpd	$$⊢\phi \to O\in \mathrm{Grp}$$
40	14 27 39	grpidcld	$$⊢\phi \to 0_O\in {\mathrm{Base}}_O$$
41	37 40	ifcld	$$⊢\phi \to if\left(n=I\times \left\{0\right\},A\left(X\right),0_O\right)\in {\mathrm{Base}}_O$$
42	41	adantr	$$⊢\left(\phi \wedge n\in D\right)\to if\left(n=I\times \left\{0\right\},A\left(X\right),0_O\right)\in {\mathrm{Base}}_O$$
43	38 42	fmpt3d	$$⊢\phi \to C\left(A\left(X\right)\right):D⟶{\mathrm{Base}}_O$$
44	43	ffnd	$$⊢\phi \to C\left(A\left(X\right)\right)FnD$$
45		eqeq2	$$⊢\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right)=if\left(n=I\times \left\{0\right\},\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right),E\times \left\{0_R\right\}\right)\to \left(\left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right)\leftrightarrow \left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=if\left(n=I\times \left\{0\right\},\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right),E\times \left\{0_R\right\}\right)\right)$$
46		eqeq2	$$⊢E\times \left\{0_R\right\}=if\left(n=I\times \left\{0\right\},\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right),E\times \left\{0_R\right\}\right)\to \left(\left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=E\times \left\{0_R\right\}\leftrightarrow \left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=if\left(n=I\times \left\{0\right\},\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right),E\times \left\{0_R\right\}\right)\right)$$
47		simpr	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge n=I\times \left\{0\right\}\right)\to n=I\times \left\{0\right\}$$
48	47	iftrued	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge n=I\times \left\{0\right\}\right)\to if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)=if\left(m=J\times \left\{0\right\},X,0_R\right)$$
49	48	mpteq2dv	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge n=I\times \left\{0\right\}\right)\to \left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right)$$
50		simpr	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge \neg n=I\times \left\{0\right\}\right)\to \neg n=I\times \left\{0\right\}$$
51	50	iffalsed	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge \neg n=I\times \left\{0\right\}\right)\to if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)=0_R$$
52	51	mpteq2dv	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge \neg n=I\times \left\{0\right\}\right)\to \left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=\left(m\in E⟼0_R\right)$$
53		fconstmpt	$$⊢E\times \left\{0_R\right\}=\left(m\in E⟼0_R\right)$$
54	52 53	eqtr4di	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge \neg n=I\times \left\{0\right\}\right)\to \left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=E\times \left\{0_R\right\}$$
55	45 46 49 54	ifbothda	$$⊢\left(\phi \wedge n\in D\right)\to \left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)=if\left(n=I\times \left\{0\right\},\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right),E\times \left\{0_R\right\}\right)$$
56	15	adantr	$$⊢\left(\phi \wedge n\in D\right)\to J\in \mathrm{V}$$
57	16	adantr	$$⊢\left(\phi \wedge n\in D\right)\to R\in \mathrm{Ring}$$
58	24	ffvelcdmda	$$⊢\left(\phi \wedge n\in D\right)\to B\left(X\right)\left(n\right)\in S$$
59	2 9 18 1 5 56 57 58	mplascl	$$⊢\left(\phi \wedge n\in D\right)\to A\left(B\left(X\right)\left(n\right)\right)=\left(m\in E⟼if\left(m=J\times \left\{0\right\},B\left(X\right)\left(n\right),0_R\right)\right)$$
60	19 23	fvmpt2d	$$⊢\left(\phi \wedge n\in D\right)\to B\left(X\right)\left(n\right)=if\left(n=I\times \left\{0\right\},X,0_R\right)$$
61	60	adantr	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge m\in E\right)\to B\left(X\right)\left(n\right)=if\left(n=I\times \left\{0\right\},X,0_R\right)$$
62	61	ifeq1d	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge m\in E\right)\to if\left(m=J\times \left\{0\right\},B\left(X\right)\left(n\right),0_R\right)=if\left(m=J\times \left\{0\right\},if\left(n=I\times \left\{0\right\},X,0_R\right),0_R\right)$$
63		ififcom	$$⊢if\left(m=J\times \left\{0\right\},if\left(n=I\times \left\{0\right\},X,0_R\right),0_R\right)=if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)$$
64	62 63	eqtrdi	$$⊢\left(\left(\phi \wedge n\in D\right)\wedge m\in E\right)\to if\left(m=J\times \left\{0\right\},B\left(X\right)\left(n\right),0_R\right)=if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)$$
65	64	mpteq2dva	$$⊢\left(\phi \wedge n\in D\right)\to \left(m\in E⟼if\left(m=J\times \left\{0\right\},B\left(X\right)\left(n\right),0_R\right)\right)=\left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)$$
66	59 65	eqtrd	$$⊢\left(\phi \wedge n\in D\right)\to A\left(B\left(X\right)\left(n\right)\right)=\left(m\in E⟼if\left(n=I\times \left\{0\right\},if\left(m=J\times \left\{0\right\},X,0_R\right),0_R\right)\right)$$
67	2 9 18 1 5 15 16 13	mplascl	$$⊢\phi \to A\left(X\right)=\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right)$$
68	2 9 18 27 15 20	mpl0	$$⊢\phi \to 0_O=E\times \left\{0_R\right\}$$
69	67 68	ifeq12d	$$⊢\phi \to if\left(n=I\times \left\{0\right\},A\left(X\right),0_O\right)=if\left(n=I\times \left\{0\right\},\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right),E\times \left\{0_R\right\}\right)$$
70	69	adantr	$$⊢\left(\phi \wedge n\in D\right)\to if\left(n=I\times \left\{0\right\},A\left(X\right),0_O\right)=if\left(n=I\times \left\{0\right\},\left(m\in E⟼if\left(m=J\times \left\{0\right\},X,0_R\right)\right),E\times \left\{0_R\right\}\right)$$
71	55 66 70	3eqtr4d	$$⊢\left(\phi \wedge n\in D\right)\to A\left(B\left(X\right)\left(n\right)\right)=if\left(n=I\times \left\{0\right\},A\left(X\right),0_O\right)$$
72	24	adantr	$$⊢\left(\phi \wedge n\in D\right)\to B\left(X\right):D⟶S$$
73		simpr	$$⊢\left(\phi \wedge n\in D\right)\to n\in D$$
74	72 73	fvco3d	$$⊢\left(\phi \wedge n\in D\right)\to \left(A\circ B\left(X\right)\right)\left(n\right)=A\left(B\left(X\right)\left(n\right)\right)$$
75	38 42	fvmpt2d	$$⊢\left(\phi \wedge n\in D\right)\to C\left(A\left(X\right)\right)\left(n\right)=if\left(n=I\times \left\{0\right\},A\left(X\right),0_O\right)$$
76	71 74 75	3eqtr4d	$$⊢\left(\phi \wedge n\in D\right)\to \left(A\circ B\left(X\right)\right)\left(n\right)=C\left(A\left(X\right)\right)\left(n\right)$$
77	26 44 76	eqfnfvd	$$⊢\phi \to A\circ B\left(X\right)=C\left(A\left(X\right)\right)$$