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 )