This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( 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 ) ) )