Metamath Proof Explorer

Theorem pwsco2mhm

Description: Left composition with a monoid homomorphism yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pwsco2mhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐴 )
pwsco2mhm.z ⊢ 𝑍 = ( 𝑆 ↑s 𝐴 )
pwsco2mhm.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwsco2mhm.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
pwsco2mhm.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) )
Assertion pwsco2mhm ( 𝜑 → ( 𝑔 ∈ 𝐵 ↦ ( 𝐹 ∘ 𝑔 ) ) ∈ ( 𝑌 MndHom 𝑍 ) )

Proof

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