MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mhmmnd Structured version   Visualization version   GIF version

Theorem mhmmnd 18221
Description: The image of a monoid 𝐺 under a monoid homomorphism 𝐹 is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020.)
Hypotheses
Ref Expression
ghmgrp.f ((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
ghmgrp.x 𝑋 = (Base‘𝐺)
ghmgrp.y 𝑌 = (Base‘𝐻)
ghmgrp.p + = (+g𝐺)
ghmgrp.q = (+g𝐻)
ghmgrp.1 (𝜑𝐹:𝑋onto𝑌)
mhmmnd.3 (𝜑𝐺 ∈ Mnd)
Assertion
Ref Expression
mhmmnd (𝜑𝐻 ∈ Mnd)
Distinct variable groups:   𝑥,𝐹,𝑦   𝑥,𝐺,𝑦   𝑥, + ,𝑦   𝑥,𝐻,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝑥, ,𝑦   𝜑,𝑥,𝑦

Proof of Theorem mhmmnd
Dummy variables 𝑎 𝑑 𝑖 𝑗 𝑘 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpllr 775 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑖) = 𝑎)
2 simpr 488 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑗) = 𝑏)
31, 2oveq12d 7167 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
4 simp-5l 784 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝜑)
5 ghmgrp.f . . . . . . . . . 10 ((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
64, 5syl3an1 1160 . . . . . . . . 9 (((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
7 simp-4r 783 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑖𝑋)
8 simplr 768 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑗𝑋)
96, 7, 8mhmlem 18219 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
10 ghmgrp.1 . . . . . . . . . . 11 (𝜑𝐹:𝑋onto𝑌)
11 fof 6581 . . . . . . . . . . 11 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
1210, 11syl 17 . . . . . . . . . 10 (𝜑𝐹:𝑋𝑌)
1312ad5antr 733 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐹:𝑋𝑌)
14 mhmmnd.3 . . . . . . . . . . 11 (𝜑𝐺 ∈ Mnd)
1514ad5antr 733 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐺 ∈ Mnd)
16 ghmgrp.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
17 ghmgrp.p . . . . . . . . . . 11 + = (+g𝐺)
1816, 17mndcl 17919 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋𝑗𝑋) → (𝑖 + 𝑗) ∈ 𝑋)
1915, 7, 8, 18syl3anc 1368 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑖 + 𝑗) ∈ 𝑋)
2013, 19ffvelrnd 6843 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) ∈ 𝑌)
219, 20eqeltrrd 2917 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) ∈ 𝑌)
223, 21eqeltrrd 2917 . . . . . 6 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑎 𝑏) ∈ 𝑌)
23 simpr 488 . . . . . . . 8 ((𝑎𝑌𝑏𝑌) → 𝑏𝑌)
24 foelrni 6718 . . . . . . . 8 ((𝐹:𝑋onto𝑌𝑏𝑌) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2510, 23, 24syl2an 598 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2625ad2antrr 725 . . . . . 6 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2722, 26r19.29a 3281 . . . . 5 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 𝑏) ∈ 𝑌)
28 simpl 486 . . . . . 6 ((𝑎𝑌𝑏𝑌) → 𝑎𝑌)
29 foelrni 6718 . . . . . 6 ((𝐹:𝑋onto𝑌𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3010, 28, 29syl2an 598 . . . . 5 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3127, 30r19.29a 3281 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → (𝑎 𝑏) ∈ 𝑌)
32 simpll 766 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝜑)
33 simplrl 776 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑎𝑌)
34 simplrr 777 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑏𝑌)
35 simpr 488 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑐𝑌)
3614ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) → 𝐺 ∈ Mnd)
3736ad5antr 733 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝐺 ∈ Mnd)
38 simp-6r 787 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑖𝑋)
39 simp-4r 783 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑗𝑋)
40 simplr 768 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑘𝑋)
4116, 17mndass 17920 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑖𝑋𝑗𝑋𝑘𝑋)) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4237, 38, 39, 40, 41syl13anc 1369 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4342fveq2d 6665 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = (𝐹‘(𝑖 + (𝑗 + 𝑘))))
44 simp-7l 788 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝜑)
4544, 5syl3an1 1160 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
4637, 38, 39, 18syl3anc 1368 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑖 + 𝑗) ∈ 𝑋)
4745, 46, 40mhmlem 18219 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)))
4816, 17mndcl 17919 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑗𝑋𝑘𝑋) → (𝑗 + 𝑘) ∈ 𝑋)
4937, 39, 40, 48syl3anc 1368 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑗 + 𝑘) ∈ 𝑋)
5045, 38, 49mhmlem 18219 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + (𝑗 + 𝑘))) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
5143, 47, 503eqtr3d 2867 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
52 simp1 1133 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋𝑗𝑋) → 𝜑)
5352, 5syl3an1 1160 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋𝑗𝑋) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
54 simp2 1134 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑖𝑋)
55 simp3 1135 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑗𝑋)
5653, 54, 55mhmlem 18219 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋𝑗𝑋) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5744, 38, 39, 56syl3anc 1368 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5857oveq1d 7164 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)))
5945, 39, 40mhmlem 18219 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑗 + 𝑘)) = ((𝐹𝑗) (𝐹𝑘)))
6059oveq2d 7165 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
6151, 58, 603eqtr3d 2867 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
62 simp-5r 785 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑖) = 𝑎)
63 simpllr 775 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑗) = 𝑏)
6462, 63oveq12d 7167 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
65 simpr 488 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑘) = 𝑐)
6664, 65oveq12d 7167 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝑎 𝑏) 𝑐))
6763, 65oveq12d 7167 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑗) (𝐹𝑘)) = (𝑏 𝑐))
6862, 67oveq12d 7167 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))) = (𝑎 (𝑏 𝑐)))
6961, 66, 683eqtr3d 2867 . . . . . . . . 9 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
70 foelrni 6718 . . . . . . . . . . . 12 ((𝐹:𝑋onto𝑌𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7110, 70sylan 583 . . . . . . . . . . 11 ((𝜑𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
72713ad2antr3 1187 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7372ad4antr 731 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7469, 73r19.29a 3281 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
75253adantr3 1168 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7675ad2antrr 725 . . . . . . . 8 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7774, 76r19.29a 3281 . . . . . . 7 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
78303adantr3 1168 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
7977, 78r19.29a 3281 . . . . . 6 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8032, 33, 34, 35, 79syl13anc 1369 . . . . 5 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8180ralrimiva 3177 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8231, 81jca 515 . . 3 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
8382ralrimivva 3186 . 2 (𝜑 → ∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
84 eqid 2824 . . . . . 6 (0g𝐺) = (0g𝐺)
8516, 84mndidcl 17926 . . . . 5 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝑋)
8614, 85syl 17 . . . 4 (𝜑 → (0g𝐺) ∈ 𝑋)
8712, 86ffvelrnd 6843 . . 3 (𝜑 → (𝐹‘(0g𝐺)) ∈ 𝑌)
88 simplll 774 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝜑)
8988, 5syl3an1 1160 . . . . . . . . 9 (((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
9014ad3antrrr 729 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝐺 ∈ Mnd)
9190, 85syl 17 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (0g𝐺) ∈ 𝑋)
92 simplr 768 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝑖𝑋)
9389, 91, 92mhmlem 18219 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = ((𝐹‘(0g𝐺)) (𝐹𝑖)))
9416, 17, 84mndlid 17931 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → ((0g𝐺) + 𝑖) = 𝑖)
9590, 92, 94syl2anc 587 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((0g𝐺) + 𝑖) = 𝑖)
9695fveq2d 6665 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = (𝐹𝑖))
9793, 96eqtr3d 2861 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = (𝐹𝑖))
98 simpr 488 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹𝑖) = 𝑎)
9998oveq2d 7165 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = ((𝐹‘(0g𝐺)) 𝑎))
10097, 99, 983eqtr3d 2867 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) 𝑎) = 𝑎)
10189, 92, 91mhmlem 18219 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = ((𝐹𝑖) (𝐹‘(0g𝐺))))
10216, 17, 84mndrid 17932 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → (𝑖 + (0g𝐺)) = 𝑖)
10390, 92, 102syl2anc 587 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑖 + (0g𝐺)) = 𝑖)
104103fveq2d 6665 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = (𝐹𝑖))
105101, 104eqtr3d 2861 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝐹𝑖))
10698oveq1d 7164 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝑎 (𝐹‘(0g𝐺))))
107105, 106, 983eqtr3d 2867 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 (𝐹‘(0g𝐺))) = 𝑎)
108100, 107jca 515 . . . . 5 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
10910, 29sylan 583 . . . . 5 ((𝜑𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
110108, 109r19.29a 3281 . . . 4 ((𝜑𝑎𝑌) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
111110ralrimiva 3177 . . 3 (𝜑 → ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
112 oveq1 7156 . . . . . 6 (𝑑 = (𝐹‘(0g𝐺)) → (𝑑 𝑎) = ((𝐹‘(0g𝐺)) 𝑎))
113112eqeq1d 2826 . . . . 5 (𝑑 = (𝐹‘(0g𝐺)) → ((𝑑 𝑎) = 𝑎 ↔ ((𝐹‘(0g𝐺)) 𝑎) = 𝑎))
114113ovanraleqv 7173 . . . 4 (𝑑 = (𝐹‘(0g𝐺)) → (∀𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎) ↔ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)))
115114rspcev 3609 . . 3 (((𝐹‘(0g𝐺)) ∈ 𝑌 ∧ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)) → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
11687, 111, 115syl2anc 587 . 2 (𝜑 → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
117 ghmgrp.y . . 3 𝑌 = (Base‘𝐻)
118 ghmgrp.q . . 3 = (+g𝐻)
119117, 118ismnd 17914 . 2 (𝐻 ∈ Mnd ↔ (∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))) ∧ ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎)))
12083, 116, 119sylanbrc 586 1 (𝜑𝐻 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  wral 3133  wrex 3134  wf 6339  ontowfo 6341  cfv 6343  (class class class)co 7149  Basecbs 16483  +gcplusg 16565  0gc0g 16713  Mndcmnd 17911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-fo 6349  df-fv 6351  df-riota 7107  df-ov 7152  df-0g 16715  df-mgm 17852  df-sgrp 17901  df-mnd 17912
This theorem is referenced by:  mhmfmhm  18222  ghmgrp  18223  ghmcmn  18952
  Copyright terms: Public domain W3C validator