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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐵 )
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 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
73 7 5 72 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
74 73 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → 𝐹 ∈ V )
75 coexg ⊢ ( ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∈ V ∧ 𝐹 ∈ V ) → ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) ∈ V )
76 71 74 75 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) ∈ V )
77 66 67 70 76 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ∘ 𝐹 ) )
78 coeq1 ⊢ ( 𝑔 = 𝑥 → ( 𝑔 ∘ 𝐹 ) = ( 𝑥 ∘ 𝐹 ) )
79 coexg ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝐹 ∈ V ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
80 33 74 79 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑥 ∘ 𝐹 ) ∈ V )
81 66 78 33 80 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) = ( 𝑥 ∘ 𝐹 ) )
82 coeq1 ⊢ ( 𝑔 = 𝑦 → ( 𝑔 ∘ 𝐹 ) = ( 𝑦 ∘ 𝐹 ) )
83 coexg ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝐹 ∈ V ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
84 38 74 83 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( 𝑦 ∘ 𝐹 ) ∈ V )
85 66 82 38 84 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) = ( 𝑦 ∘ 𝐹 ) )
86 81 85 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) = ( ( 𝑥 ∘ 𝐹 ) ( +g ‘ 𝑌 ) ( 𝑦 ∘ 𝐹 ) ) )
87 65 77 86 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) ) → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) )
88 87 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) )
89 coeq1 ⊢ ( 𝑔 = ( 0g ‘ 𝑍 ) → ( 𝑔 ∘ 𝐹 ) = ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) )
90 eqid ⊢ ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 )
91 3 90 mndidcl ⊢ ( 𝑍 ∈ Mnd → ( 0g ‘ 𝑍 ) ∈ 𝐶 )
92 9 91 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑍 ) ∈ 𝐶 )
93 coexg ⊢ ( ( ( 0g ‘ 𝑍 ) ∈ 𝐶 ∧ 𝐹 ∈ V ) → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ∈ V )
94 92 73 93 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ∈ V )
95 66 89 92 94 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) )
96 2 12 3 4 6 92 pwselbas ⊢ ( 𝜑 → ( 0g ‘ 𝑍 ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) )
97 fco ⊢ ( ( ( 0g ‘ 𝑍 ) : 𝐵 ⟶ ( Base ‘ 𝑅 ) ∧ 𝐹 : 𝐴 ⟶ 𝐵 ) → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
98 96 7 97 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝑅 ) )
99 98 ffnd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) Fn 𝐴 )
100 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
101 fnconstg ⊢ ( ( 0g ‘ 𝑅 ) ∈ V → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) Fn 𝐴 )
102 100 101 syl ⊢ ( 𝜑 → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) Fn 𝐴 )
103 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
104 2 103 pws0g ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑍 ) )
105 4 6 104 syl2anc ⊢ ( 𝜑 → ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑍 ) )
106 105 fveq1d ⊢ ( 𝜑 → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
108 fvex ⊢ ( 0g ‘ 𝑅 ) ∈ V
109 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
110 fvconst2g ⊢ ( ( ( 0g ‘ 𝑅 ) ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
111 108 109 110 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐵 × { ( 0g ‘ 𝑅 ) } ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
112 107 111 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ 𝑅 ) )
113 fvco3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
114 7 113 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 0g ‘ 𝑍 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
115 fvconst2g ⊢ ( ( ( 0g ‘ 𝑅 ) ∈ V ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
116 100 115 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑥 ) = ( 0g ‘ 𝑅 ) )
117 112 114 116 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) ‘ 𝑥 ) )
118 99 102 117 eqfnfvd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑍 ) ∘ 𝐹 ) = ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) )
119 1 103 pws0g ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑌 ) )
120 4 5 119 syl2anc ⊢ ( 𝜑 → ( 𝐴 × { ( 0g ‘ 𝑅 ) } ) = ( 0g ‘ 𝑌 ) )
121 95 118 120 3eqtrd ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑌 ) )
122 24 88 121 3jca ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) : 𝐶 ⟶ ( Base ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑌 ) ) )
123 eqid ⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
124 3 19 57 55 90 123 ismhm ⊢ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( 𝑍 MndHom 𝑌 ) ↔ ( ( 𝑍 ∈ Mnd ∧ 𝑌 ∈ Mnd ) ∧ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) : 𝐶 ⟶ ( Base ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ 𝐶 ∀ 𝑦 ∈ 𝐶 ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 𝑥 ( +g ‘ 𝑍 ) 𝑦 ) ) = ( ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑥 ) ( +g ‘ 𝑌 ) ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ 𝑦 ) ) ∧ ( ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑌 ) ) ) )
125 9 11 122 124 syl21anbrc ⊢ ( 𝜑 → ( 𝑔 ∈ 𝐶 ↦ ( 𝑔 ∘ 𝐹 ) ) ∈ ( 𝑍 MndHom 𝑌 ) )