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 = ( Base ` R )
	mplasclco.o	\|- O = ( J mPoly R )
	mplasclco.p	\|- P = ( I mPoly R )
	mplasclco.q	\|- Q = ( I mPoly O )
	mplasclco.a	\|- A = ( algSc ` O )
	mplasclco.b	\|- B = ( algSc ` P )
	mplasclco.c	\|- C = ( algSc ` Q )
	mplasclco.d	\|- D = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
	mplasclco.e	\|- E = { j e. ( NN0 ^m J ) \| ( `' j " NN ) e. Fin }
	mplasclco.i	\|- ( ph -> I e. V )
	mplasclco.j	\|- ( ph -> J C_ I )
	mplasclco.r	\|- ( ph -> R e. CRing )
	mplasclco.x	\|- ( ph -> X e. S )
Assertion	mplasclco	\|- ( ph -> ( A o. ( B ` X ) ) = ( C ` ( A ` X ) ) )

Proof

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

Metamath Proof Explorer

Theorem mplasclco

Proof