Metamath Proof Explorer

Theorem mhmmnd

Description: The image of a monoid G under a monoid homomorphism F is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020)

Ref Expression
Hypotheses ghmgrp.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
ghmgrp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
ghmgrp.y ⊢ 𝑌 = ( Base ‘ 𝐻 )
ghmgrp.p ⊢ + = ( +g ‘ 𝐺 )
ghmgrp.q ⊢ ⨣ = ( +g ‘ 𝐻 )
ghmgrp.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
mhmmnd.3 ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
Assertion mhmmnd ( 𝜑 → 𝐻 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 ghmgrp.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
2 ghmgrp.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
3 ghmgrp.y ⊢ 𝑌 = ( Base ‘ 𝐻 )
4 ghmgrp.p ⊢ + = ( +g ‘ 𝐺 )
5 ghmgrp.q ⊢ ⨣ = ( +g ‘ 𝐻 )
6 ghmgrp.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
7 mhmmnd.3 ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
8 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( 𝐹 ‘ 𝑖 ) = 𝑎 )
9 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( 𝐹 ‘ 𝑗 ) = 𝑏 )
10 8 9 oveq12d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) = ( 𝑎 ⨣ 𝑏 ) )
11 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → 𝜑 )
12 11 1 syl3an1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
13 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → 𝑖 ∈ 𝑋 )
14 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → 𝑗 ∈ 𝑋 )
15 12 13 14 mhmlem ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( 𝐹 ‘ ( 𝑖 + 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) )
16 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
17 6 16 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
18 17 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → 𝐹 : 𝑋 ⟶ 𝑌 )
19 7 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → 𝐺 ∈ Mnd )
20 2 4 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑋 ) → ( 𝑖 + 𝑗 ) ∈ 𝑋 )
21 19 13 14 20 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( 𝑖 + 𝑗 ) ∈ 𝑋 )
22 18 21 ffvelrnd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( 𝐹 ‘ ( 𝑖 + 𝑗 ) ) ∈ 𝑌 )
23 15 22 eqeltrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) ∈ 𝑌 )
24 10 23 eqeltrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝑌 )
25 simpr ⊢ ( ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) → 𝑏 ∈ 𝑌 )
26 foelrni ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑏 ∈ 𝑌 ) → ∃ 𝑗 ∈ 𝑋 ( 𝐹 ‘ 𝑗 ) = 𝑏 )
27 6 25 26 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) → ∃ 𝑗 ∈ 𝑋 ( 𝐹 ‘ 𝑗 ) = 𝑏 )
28 27 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ∃ 𝑗 ∈ 𝑋 ( 𝐹 ‘ 𝑗 ) = 𝑏 )
29 24 28 r19.29a ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝑌 )
30 simpl ⊢ ( ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) → 𝑎 ∈ 𝑌 )
31 foelrni ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑎 ∈ 𝑌 ) → ∃ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) = 𝑎 )
32 6 30 31 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) → ∃ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) = 𝑎 )
33 29 32 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) → ( 𝑎 ⨣ 𝑏 ) ∈ 𝑌 )
34 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑐 ∈ 𝑌 ) → 𝜑 )
35 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑐 ∈ 𝑌 ) → 𝑎 ∈ 𝑌 )
36 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑐 ∈ 𝑌 ) → 𝑏 ∈ 𝑌 )
37 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑐 ∈ 𝑌 ) → 𝑐 ∈ 𝑌 )
38 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) → 𝐺 ∈ Mnd )
39 38 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → 𝐺 ∈ Mnd )
40 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → 𝑖 ∈ 𝑋 )
41 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → 𝑗 ∈ 𝑋 )
42 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → 𝑘 ∈ 𝑋 )
43 2 4 mndass ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) ) → ( ( 𝑖 + 𝑗 ) + 𝑘 ) = ( 𝑖 + ( 𝑗 + 𝑘 ) ) )
44 39 40 41 42 43 syl13anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝑖 + 𝑗 ) + 𝑘 ) = ( 𝑖 + ( 𝑗 + 𝑘 ) ) )
45 44 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ ( ( 𝑖 + 𝑗 ) + 𝑘 ) ) = ( 𝐹 ‘ ( 𝑖 + ( 𝑗 + 𝑘 ) ) ) )
46 simp-7l ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → 𝜑 )
47 46 1 syl3an1 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
48 39 40 41 20 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝑖 + 𝑗 ) ∈ 𝑋 )
49 47 48 42 mhmlem ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ ( ( 𝑖 + 𝑗 ) + 𝑘 ) ) = ( ( 𝐹 ‘ ( 𝑖 + 𝑗 ) ) ⨣ ( 𝐹 ‘ 𝑘 ) ) )
50 2 4 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝑋 ∧ 𝑘 ∈ 𝑋 ) → ( 𝑗 + 𝑘 ) ∈ 𝑋 )
51 39 41 42 50 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝑗 + 𝑘 ) ∈ 𝑋 )
52 47 40 51 mhmlem ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ ( 𝑖 + ( 𝑗 + 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ ( 𝑗 + 𝑘 ) ) ) )
53 45 49 52 3eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝐹 ‘ ( 𝑖 + 𝑗 ) ) ⨣ ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ ( 𝑗 + 𝑘 ) ) ) )
54 simp1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑋 ) → 𝜑 )
55 54 1 syl3an1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
56 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑋 ) → 𝑖 ∈ 𝑋 )
57 simp3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑋 ) → 𝑗 ∈ 𝑋 )
58 55 56 57 mhmlem ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑋 ∧ 𝑗 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑖 + 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) )
59 46 40 41 58 syl3anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ ( 𝑖 + 𝑗 ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) )
60 59 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝐹 ‘ ( 𝑖 + 𝑗 ) ) ⨣ ( 𝐹 ‘ 𝑘 ) ) = ( ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) ⨣ ( 𝐹 ‘ 𝑘 ) ) )
61 47 41 42 mhmlem ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ ( 𝑗 + 𝑘 ) ) = ( ( 𝐹 ‘ 𝑗 ) ⨣ ( 𝐹 ‘ 𝑘 ) ) )
62 61 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ ( 𝑗 + 𝑘 ) ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( ( 𝐹 ‘ 𝑗 ) ⨣ ( 𝐹 ‘ 𝑘 ) ) ) )
63 53 60 62 3eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) ⨣ ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( ( 𝐹 ‘ 𝑗 ) ⨣ ( 𝐹 ‘ 𝑘 ) ) ) )
64 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ 𝑖 ) = 𝑎 )
65 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ 𝑗 ) = 𝑏 )
66 64 65 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) = ( 𝑎 ⨣ 𝑏 ) )
67 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( 𝐹 ‘ 𝑘 ) = 𝑐 )
68 66 67 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ 𝑗 ) ) ⨣ ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) )
69 65 67 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝐹 ‘ 𝑗 ) ⨣ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑏 ⨣ 𝑐 ) )
70 64 69 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝐹 ‘ 𝑖 ) ⨣ ( ( 𝐹 ‘ 𝑗 ) ⨣ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) )
71 63 68 70 3eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) ∧ 𝑘 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) = 𝑐 ) → ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) )
72 foelrni ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑐 ∈ 𝑌 ) → ∃ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) = 𝑐 )
73 6 72 sylan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑌 ) → ∃ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) = 𝑐 )
74 73 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) → ∃ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) = 𝑐 )
75 74 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ∃ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) = 𝑐 )
76 71 75 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑗 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑗 ) = 𝑏 ) → ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) )
77 27 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) → ∃ 𝑗 ∈ 𝑋 ( 𝐹 ‘ 𝑗 ) = 𝑏 )
78 77 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ∃ 𝑗 ∈ 𝑋 ( 𝐹 ‘ 𝑗 ) = 𝑏 )
79 76 78 r19.29a ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) )
80 32 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) → ∃ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) = 𝑎 )
81 79 80 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ∧ 𝑐 ∈ 𝑌 ) ) → ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) )
82 34 35 36 37 81 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) ∧ 𝑐 ∈ 𝑌 ) → ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) )
83 82 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) → ∀ 𝑐 ∈ 𝑌 ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) )
84 33 83 jca ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑏 ∈ 𝑌 ) ) → ( ( 𝑎 ⨣ 𝑏 ) ∈ 𝑌 ∧ ∀ 𝑐 ∈ 𝑌 ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) ) )
85 84 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑌 ∀ 𝑏 ∈ 𝑌 ( ( 𝑎 ⨣ 𝑏 ) ∈ 𝑌 ∧ ∀ 𝑐 ∈ 𝑌 ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) ) )
86 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
87 2 86 mndidcl ⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
88 7 87 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
89 17 88 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ∈ 𝑌 )
90 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → 𝜑 )
91 90 1 syl3an1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
92 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → 𝐺 ∈ Mnd )
93 92 87 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
94 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → 𝑖 ∈ 𝑋 )
95 91 93 94 mhmlem ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( ( 0g ‘ 𝐺 ) + 𝑖 ) ) = ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ ( 𝐹 ‘ 𝑖 ) ) )
96 2 4 86 mndlid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑖 ∈ 𝑋 ) → ( ( 0g ‘ 𝐺 ) + 𝑖 ) = 𝑖 )
97 92 94 96 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 0g ‘ 𝐺 ) + 𝑖 ) = 𝑖 )
98 97 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( ( 0g ‘ 𝐺 ) + 𝑖 ) ) = ( 𝐹 ‘ 𝑖 ) )
99 95 98 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ ( 𝐹 ‘ 𝑖 ) ) = ( 𝐹 ‘ 𝑖 ) )
100 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ 𝑖 ) = 𝑎 )
101 100 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) )
102 99 101 100 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) = 𝑎 )
103 91 94 93 mhmlem ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( 𝑖 + ( 0g ‘ 𝐺 ) ) ) = ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) )
104 2 4 86 mndrid ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑖 ∈ 𝑋 ) → ( 𝑖 + ( 0g ‘ 𝐺 ) ) = 𝑖 )
105 92 94 104 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝑖 + ( 0g ‘ 𝐺 ) ) = 𝑖 )
106 105 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝐹 ‘ ( 𝑖 + ( 0g ‘ 𝐺 ) ) ) = ( 𝐹 ‘ 𝑖 ) )
107 103 106 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = ( 𝐹 ‘ 𝑖 ) )
108 100 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( 𝐹 ‘ 𝑖 ) ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = ( 𝑎 ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) )
109 107 108 100 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( 𝑎 ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = 𝑎 )
110 102 109 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) ∧ 𝑖 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑖 ) = 𝑎 ) → ( ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = 𝑎 ) )
111 6 31 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) → ∃ 𝑖 ∈ 𝑋 ( 𝐹 ‘ 𝑖 ) = 𝑎 )
112 110 111 r19.29a ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑌 ) → ( ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = 𝑎 ) )
113 112 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑌 ( ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = 𝑎 ) )
114 oveq1 ⊢ ( 𝑑 = ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) → ( 𝑑 ⨣ 𝑎 ) = ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) )
115 114 eqeq1d ⊢ ( 𝑑 = ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) → ( ( 𝑑 ⨣ 𝑎 ) = 𝑎 ↔ ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) = 𝑎 ) )
116 115 ovanraleqv ⊢ ( 𝑑 = ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) → ( ∀ 𝑎 ∈ 𝑌 ( ( 𝑑 ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ 𝑑 ) = 𝑎 ) ↔ ∀ 𝑎 ∈ 𝑌 ( ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = 𝑎 ) ) )
117 116 rspcev ⊢ ( ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ∈ 𝑌 ∧ ∀ 𝑎 ∈ 𝑌 ( ( ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) ) = 𝑎 ) ) → ∃ 𝑑 ∈ 𝑌 ∀ 𝑎 ∈ 𝑌 ( ( 𝑑 ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ 𝑑 ) = 𝑎 ) )
118 89 113 117 syl2anc ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑌 ∀ 𝑎 ∈ 𝑌 ( ( 𝑑 ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ 𝑑 ) = 𝑎 ) )
119 3 5 ismnd ⊢ ( 𝐻 ∈ Mnd ↔ ( ∀ 𝑎 ∈ 𝑌 ∀ 𝑏 ∈ 𝑌 ( ( 𝑎 ⨣ 𝑏 ) ∈ 𝑌 ∧ ∀ 𝑐 ∈ 𝑌 ( ( 𝑎 ⨣ 𝑏 ) ⨣ 𝑐 ) = ( 𝑎 ⨣ ( 𝑏 ⨣ 𝑐 ) ) ) ∧ ∃ 𝑑 ∈ 𝑌 ∀ 𝑎 ∈ 𝑌 ( ( 𝑑 ⨣ 𝑎 ) = 𝑎 ∧ ( 𝑎 ⨣ 𝑑 ) = 𝑎 ) ) )
120 85 118 119 sylanbrc ⊢ ( 𝜑 → 𝐻 ∈ Mnd )