Metamath Proof Explorer

Theorem pwsco1mhm

Description: Right composition with a function on the index sets yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pwsco1mhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐴 )
pwsco1mhm.z ⊢ 𝑍 = ( 𝑅 ↑s 𝐵 )
pwsco1mhm.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
pwsco1mhm.r ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
pwsco1mhm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
pwsco1mhm.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
pwsco1mhm.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion pwsco1mhm ( 𝜑 → ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( 𝑍 MndHom 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pwsco1mhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐴 )
2 pwsco1mhm.z ⊢ 𝑍 = ( 𝑅 ↑s 𝐵 )
3 pwsco1mhm.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
4 pwsco1mhm.r ⊢ ( 𝜑 → 𝑅 ∈ Mnd )
5 pwsco1mhm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 pwsco1mhm.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
7 pwsco1mhm.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 2 pwsmnd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊 ) → 𝑍 ∈ Mnd )
9 4 6 8 syl2anc ⊢ ( 𝜑 → 𝑍 ∈ Mnd )
10 1 pwsmnd ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → 𝑌 ∈ Mnd )
11 4 5 10 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ Mnd )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 2 12 3 pwselbasb ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊 ) → ( 𝑔 ∈ 𝐶 ↔ 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑅 ) ) )
14 4 6 13 syl2anc ⊢ ( 𝜑 → ( 𝑔 ∈ 𝐶 ↔ 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑅 ) ) )
15 14 biimpa ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
16 7 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
17 fco ⊢ ( ( 𝑔 : 𝐵 ⟶ ( Base ‘ 𝑅 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑔 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
18 15 16 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → ( 𝑔 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
19 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
20 1 12 19 pwselbasb ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑔 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) ↔ ( 𝑔 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) ) )
21 4 5 20 syl2anc ⊢ ( 𝜑 → ( ( 𝑔 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) ↔ ( 𝑔 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → ( ( 𝑔 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) ↔ ( 𝑔 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) ) )
23 18 22 mpbird ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → ( 𝑔 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) )
24 23 fmpttd ⊢ ( 𝜑 → ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) : 𝐶 ⟶ ( Base ‘ 𝑌 ) )
25 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐴 ∈ 𝑉 )
26 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ V )
27 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ V )
28 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
29 28 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
30 28 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑧 ) ) )
31 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑅 ∈ Mnd )
32 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐵 ∈ 𝑊 )
33 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 ∈ 𝐶 )
34 2 12 3 31 32 33 pwselbas ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
35 34 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑥 = ( 𝑤 ∈ 𝐵 ↦ ( 𝑥 ‘ 𝑤 ) ) )
36 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( 𝑥 ‘ 𝑤 ) = ( 𝑥 ‘ ( 𝐹 ‘ 𝑧 ) ) )
37 29 30 35 36 fmptco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∘ 𝐹 ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝑥 ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
38 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
39 2 12 3 31 32 38 pwselbas ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
40 39 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝑦 = ( 𝑤 ∈ 𝐵 ↦ ( 𝑦 ‘ 𝑤 ) ) )
41 fveq2 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( 𝑦 ‘ 𝑤 ) = ( 𝑦 ‘ ( 𝐹 ‘ 𝑧 ) ) )
42 29 30 40 41 fmptco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑦 ∘ 𝐹 ) = ( 𝑧 ∈ 𝐴 ↦ ( 𝑦 ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
43 25 26 27 37 42 offval2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ∘ 𝐹 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∘ 𝐹 ) ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑧 ) ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) )
44 fco ⊢ ( ( 𝑥 : 𝐵 ⟶ ( Base ‘ 𝑅 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑥 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
45 34 28 44 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
46 1 12 19 pwselbasb ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑥 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) ↔ ( 𝑥 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) ) )
47 31 25 46 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) ↔ ( 𝑥 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) ) )
48 45 47 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) )
49 fco ⊢ ( ( 𝑦 : 𝐵 ⟶ ( Base ‘ 𝑅 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( 𝑦 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
50 39 28 49 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑦 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
51 1 12 19 pwselbasb ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑦 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) ↔ ( 𝑦 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) ) )
52 31 25 51 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑦 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) ↔ ( 𝑦 ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) ) )
53 50 52 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑦 ∘ 𝐹 ) ∈ ( Base ‘ 𝑌 ) )
54 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
55 eqid ⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
56 1 19 31 25 48 53 54 55 pwsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ∘ 𝐹 ) ( +g ‘ 𝑌 ) ( 𝑦 ∘ 𝐹 ) ) = ( ( 𝑥 ∘ 𝐹 ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∘ 𝐹 ) ) )
57 eqid ⊢ ( +g ‘ 𝑍 ) = ( +g ‘ 𝑍 )
58 2 3 31 32 33 38 54 57 pwsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
59 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑥 ‘ 𝑤 ) ∈ V )
60 fvexd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( 𝑦 ‘ 𝑤 ) ∈ V )
61 32 59 60 35 40 offval2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑤 ∈ 𝐵 ↦ ( ( 𝑥 ‘ 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ 𝑤 ) ) ) )
62 58 61 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) = ( 𝑤 ∈ 𝐵 ↦ ( ( 𝑥 ‘ 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ 𝑤 ) ) ) )
63 36 41 oveq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑥 ‘ 𝑤 ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ 𝑤 ) ) = ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑧 ) ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
64 29 30 62 63 fmptco ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ‘ ( 𝐹 ‘ 𝑧 ) ) ( +g ‘ 𝑅 ) ( 𝑦 ‘ ( 𝐹 ‘ 𝑧 ) ) ) ) )
65 43 56 64 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) = ( ( 𝑥 ∘ 𝐹 ) ( +g ‘ 𝑌 ) ( 𝑦 ∘ 𝐹 ) ) )
66 eqid ⊢ ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) = ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) )
67 coeq1 ⊢ ( 𝑔 = ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) → ( 𝑔 ∘ 𝐹 ) = ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) )
68 3 57 mndcl ⊢ ( ( 𝑍 ∈ Mnd ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∈ 𝐶 )
69 68 3expb ⊢ ( ( 𝑍 ∈ Mnd ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∈ 𝐶 )
70 9 69 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∈ 𝐶 )
71 ovex ⊢ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∈ V
72 7 5 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
73 72 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 ∈ V )
74 coexg ⊢ ( ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∈ V ∧ 𝐹 ∈ V ) → ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) ∈ V )
75 71 73 74 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) ∈ V )
76 66 67 70 75 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) )
77 coeq1 ⊢ ( 𝑔 = 𝑥 → ( 𝑔 ∘ 𝐹 ) = ( 𝑥 ∘ 𝐹 ) )
78 coexg ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝐹 ∈ V ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
79 33 73 78 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
80 66 77 33 79 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) = ( 𝑥 ∘ 𝐹 ) )
81 coeq1 ⊢ ( 𝑔 = 𝑦 → ( 𝑔 ∘ 𝐹 ) = ( 𝑦 ∘ 𝐹 ) )
82 coexg ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝐹 ∈ V ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
83 38 73 82 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
84 66 81 38 83 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) = ( 𝑦 ∘ 𝐹 ) )
85 80 84 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) = ( ( 𝑥 ∘ 𝐹 ) ( +g ‘ 𝑌 ) ( 𝑦 ∘ 𝐹 ) ) )
86 65 76 85 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) )
87 86 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) )
88 coeq1 ⊢ ( 𝑔 = ( 0g ‘ 𝑍 ) → ( 𝑔 ∘ 𝐹 ) = ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) )
89 eqid ⊢ ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 )
90 3 89 mndidcl ⊢ ( 𝑍 ∈ Mnd → ( 0g ‘ 𝑍 ) ∈ 𝐶 )
91 9 90 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑍 ) ∈ 𝐶 )
92 coexg ⊢ ( ( ( 0g ‘ 𝑍 ) ∈ 𝐶 ∧ 𝐹 ∈ V ) → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ∈ V )
93 91 72 92 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ∈ V )
94 66 88 91 93 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) )
95 2 12 3 4 6 91 pwselbas ⊢ ( 𝜑 → ( 0g ‘ 𝑍 ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
96 fco ⊢ ( ( ( 0g ‘ 𝑍 ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
97 95 7 96 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
98 97 ffnd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) Fn 𝐴 )
99 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
100 fnconstg ⊢ ( ( 0g ‘ 𝑅 ) ∈ V → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) Fn 𝐴 )
101 99 100 syl ⊢ ( 𝜑 → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) Fn 𝐴 )
102 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
103 2 102 pws0g ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑍 ) )
104 4 6 103 syl2anc ⊢ ( 𝜑 → ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑍 ) )
105 104 fveq1d ⊢ ( 𝜑 → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
107 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
108 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
109 fvconst2g ⊢ ( ( ( 0g ‘ 𝑅 ) ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
110 107 108 109 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
111 106 110 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
112 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
113 7 112 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
114 fvconst2g ⊢ ( ( ( 0g ‘ 𝑅 ) ∈ V ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
115 99 114 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
116 111 113 115 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑥 ) )
117 98 101 116 eqfnfvd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) = ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) )
118 1 102 pws0g ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑌 ) )
119 4 5 118 syl2anc ⊢ ( 𝜑 → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑌 ) )
120 94 117 119 3eqtrd ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑌 ) )
121 24 87 120 3jca ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) : 𝐶 ⟶ ( Base ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑌 ) ) )
122 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
123 3 19 57 55 89 122 ismhm ⊢ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( 𝑍 MndHom 𝑌 ) ↔ ( ( 𝑍 ∈ Mnd ∧ 𝑌 ∈ Mnd ) ∧ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) : 𝐶 ⟶ ( Base ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑌 ) ) ) )
124 9 11 121 123 syl21anbrc ⊢ ( 𝜑 → ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( 𝑍 MndHom 𝑌 ) )