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 ⊢ 𝑆 = ( Base ‘ 𝑅 )
mplasclco.o ⊢ 𝑂 = ( 𝐽 mPoly 𝑅 )
mplasclco.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplasclco.q ⊢ 𝑄 = ( 𝐼 mPoly 𝑂 )
mplasclco.a ⊢ 𝐴 = ( algSc ‘ 𝑂 )
mplasclco.b ⊢ 𝐵 = ( algSc ‘ 𝑃 )
mplasclco.c ⊢ 𝐶 = ( algSc ‘ 𝑄 )
mplasclco.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
mplasclco.e ⊢ 𝐸 = { 𝑗 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑗 “ ℕ ) ∈ Fin }
mplasclco.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mplasclco.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
mplasclco.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
mplasclco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion mplasclco ( 𝜑 → ( 𝐴 ∘ ( 𝐵 ‘ 𝑋 ) ) = ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mplasclco.s ⊢ 𝑆 = ( Base ‘ 𝑅 )
2 mplasclco.o ⊢ 𝑂 = ( 𝐽 mPoly 𝑅 )
3 mplasclco.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
4 mplasclco.q ⊢ 𝑄 = ( 𝐼 mPoly 𝑂 )
5 mplasclco.a ⊢ 𝐴 = ( algSc ‘ 𝑂 )
6 mplasclco.b ⊢ 𝐵 = ( algSc ‘ 𝑃 )
7 mplasclco.c ⊢ 𝐶 = ( algSc ‘ 𝑄 )
8 mplasclco.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
9 mplasclco.e ⊢ 𝐸 = { 𝑗 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑗 “ ℕ ) ∈ Fin }
10 mplasclco.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11 mplasclco.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
12 mplasclco.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
13 mplasclco.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
14 eqid ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ 𝑂 )
15 10 11 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
16 12 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 2 14 1 5 15 16 mplasclf ⊢ ( 𝜑 → 𝐴 : 𝑆 ⟶ ( Base ‘ 𝑂 ) )
18 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19 3 8 18 1 6 10 16 13 mplascl ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) = ( 𝑛 ∈ 𝐷 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
20 12 crnggrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
21 1 18 20 grpidcld ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ 𝑆 )
22 13 21 ifcld ⊢ ( 𝜑 → if ( 𝑛 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ∈ 𝑆 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → if ( 𝑛 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ∈ 𝑆 )
24 19 23 fmpt3d ⊢ ( 𝜑 → ( 𝐵 ‘ 𝑋 ) : 𝐷 ⟶ 𝑆 )
25 17 24 fcod ⊢ ( 𝜑 → ( 𝐴 ∘ ( 𝐵 ‘ 𝑋 ) ) : 𝐷 ⟶ ( Base ‘ 𝑂 ) )
26 25 ffnd ⊢ ( 𝜑 → ( 𝐴 ∘ ( 𝐵 ‘ 𝑋 ) ) Fn 𝐷 )
27 eqid ⊢ ( 0g ‘ 𝑂 ) = ( 0g ‘ 𝑂 )
28 2 15 16 mplringd ⊢ ( 𝜑 → 𝑂 ∈ Ring )
29 eqid ⊢ ( Scalar ‘ 𝑂 ) = ( Scalar ‘ 𝑂 )
30 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑂 ) ) = ( Base ‘ ( Scalar ‘ 𝑂 ) )
31 2 mplassa ⊢ ( ( 𝐽 ∈ V ∧ 𝑅 ∈ CRing ) → 𝑂 ∈ AssAlg )
32 15 12 31 syl2anc ⊢ ( 𝜑 → 𝑂 ∈ AssAlg )
33 2 15 12 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑂 ) )
34 33 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑂 ) ) )
35 1 34 eqtrid ⊢ ( 𝜑 → 𝑆 = ( Base ‘ ( Scalar ‘ 𝑂 ) ) )
36 13 35 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑂 ) ) )
37 5 29 30 32 36 asclelbas ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( Base ‘ 𝑂 ) )
38 4 8 27 14 7 10 28 37 mplascl ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑛 ∈ 𝐷 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝐴 ‘ 𝑋 ) , ( 0g ‘ 𝑂 ) ) ) )
39 28 ringgrpd ⊢ ( 𝜑 → 𝑂 ∈ Grp )
40 14 27 39 grpidcld ⊢ ( 𝜑 → ( 0g ‘ 𝑂 ) ∈ ( Base ‘ 𝑂 ) )
41 37 40 ifcld ⊢ ( 𝜑 → if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝐴 ‘ 𝑋 ) , ( 0g ‘ 𝑂 ) ) ∈ ( Base ‘ 𝑂 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝐴 ‘ 𝑋 ) , ( 0g ‘ 𝑂 ) ) ∈ ( Base ‘ 𝑂 ) )
43 38 42 fmpt3d ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) : 𝐷 ⟶ ( Base ‘ 𝑂 ) )
44 43 ffnd ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) Fn 𝐷 )
45 eqeq2 ⊢ ( ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) , ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ) → ( ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) ↔ ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) , ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ) ) )
46 eqeq2 ⊢ ( ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) , ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ) → ( ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ↔ ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) , ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ) ) )
47 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑛 = ( 𝐼 × { 0 } ) ) → 𝑛 = ( 𝐼 × { 0 } ) )
48 47 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑛 = ( 𝐼 × { 0 } ) ) → if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) )
49 48 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑛 = ( 𝐼 × { 0 } ) ) → ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
50 simpr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ ¬ 𝑛 = ( 𝐼 × { 0 } ) ) → ¬ 𝑛 = ( 𝐼 × { 0 } ) )
51 50 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ ¬ 𝑛 = ( 𝐼 × { 0 } ) ) → if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
52 51 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ ¬ 𝑛 = ( 𝐼 × { 0 } ) ) → ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑚 ∈ 𝐸 ↦ ( 0g ‘ 𝑅 ) ) )
53 fconstmpt ⊢ ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) = ( 𝑚 ∈ 𝐸 ↦ ( 0g ‘ 𝑅 ) )
54 52 53 eqtr4di ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ ¬ 𝑛 = ( 𝐼 × { 0 } ) ) → ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) )
55 45 46 49 54 ifbothda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) , ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ) )
56 15 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → 𝐽 ∈ V )
57 16 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → 𝑅 ∈ Ring )
58 24 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) ∈ 𝑆 )
59 2 9 18 1 5 56 57 58 mplascl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( 𝐴 ‘ ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) ) = ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) , ( 0g ‘ 𝑅 ) ) ) )
60 19 23 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑚 ∈ 𝐸 ) → ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) )
62 61 ifeq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑚 ∈ 𝐸 ) → if ( 𝑚 = ( 𝐽 × { 0 } ) , ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑚 = ( 𝐽 × { 0 } ) , if ( 𝑛 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) )
63 ififcom ⊢ if ( 𝑚 = ( 𝐽 × { 0 } ) , if ( 𝑛 = ( 𝐼 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) )
64 62 63 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) ∧ 𝑚 ∈ 𝐸 ) → if ( 𝑚 = ( 𝐽 × { 0 } ) , ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) )
65 64 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) )
66 59 65 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( 𝐴 ‘ ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) ) = ( 𝑚 ∈ 𝐸 ↦ if ( 𝑛 = ( 𝐼 × { 0 } ) , if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) , ( 0g ‘ 𝑅 ) ) ) )
67 2 9 18 1 5 15 16 13 mplascl ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
68 2 9 18 27 15 20 mpl0 ⊢ ( 𝜑 → ( 0g ‘ 𝑂 ) = ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) )
69 67 68 ifeq12d ⊢ ( 𝜑 → if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝐴 ‘ 𝑋 ) , ( 0g ‘ 𝑂 ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) , ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝐴 ‘ 𝑋 ) , ( 0g ‘ 𝑂 ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝑚 ∈ 𝐸 ↦ if ( 𝑚 = ( 𝐽 × { 0 } ) , 𝑋 , ( 0g ‘ 𝑅 ) ) ) , ( 𝐸 × { ( 0g ‘ 𝑅 ) } ) ) )
71 55 66 70 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( 𝐴 ‘ ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝐴 ‘ 𝑋 ) , ( 0g ‘ 𝑂 ) ) )
72 24 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( 𝐵 ‘ 𝑋 ) : 𝐷 ⟶ 𝑆 )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → 𝑛 ∈ 𝐷 )
74 72 73 fvco3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝐴 ∘ ( 𝐵 ‘ 𝑋 ) ) ‘ 𝑛 ) = ( 𝐴 ‘ ( ( 𝐵 ‘ 𝑋 ) ‘ 𝑛 ) ) )
75 38 42 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝑛 ) = if ( 𝑛 = ( 𝐼 × { 0 } ) , ( 𝐴 ‘ 𝑋 ) , ( 0g ‘ 𝑂 ) ) )
76 71 74 75 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐷 ) → ( ( 𝐴 ∘ ( 𝐵 ‘ 𝑋 ) ) ‘ 𝑛 ) = ( ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 𝑛 ) )
77 26 44 76 eqfnfvd ⊢ ( 𝜑 → ( 𝐴 ∘ ( 𝐵 ‘ 𝑋 ) ) = ( 𝐶 ‘ ( 𝐴 ‘ 𝑋 ) ) )