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

Theorem mhmmnd 17745
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 760 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑖) = 𝑎)
2 simpr 471 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑗) = 𝑏)
31, 2oveq12d 6814 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
4 simp-5l 772 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝜑)
5 ghmgrp.f . . . . . . . . . 10 ((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
64, 5syl3an1 1166 . . . . . . . . 9 (((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
7 simp-4r 770 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑖𝑋)
8 simplr 752 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑗𝑋)
96, 7, 8mhmlem 17743 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
10 ghmgrp.1 . . . . . . . . . . 11 (𝜑𝐹:𝑋onto𝑌)
11 fof 6257 . . . . . . . . . . 11 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
1210, 11syl 17 . . . . . . . . . 10 (𝜑𝐹:𝑋𝑌)
1312ad5antr 716 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐹:𝑋𝑌)
14 mhmmnd.3 . . . . . . . . . . 11 (𝜑𝐺 ∈ Mnd)
1514ad5antr 716 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐺 ∈ Mnd)
16 ghmgrp.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
17 ghmgrp.p . . . . . . . . . . 11 + = (+g𝐺)
1816, 17mndcl 17509 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋𝑗𝑋) → (𝑖 + 𝑗) ∈ 𝑋)
1915, 7, 8, 18syl3anc 1476 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑖 + 𝑗) ∈ 𝑋)
2013, 19ffvelrnd 6505 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) ∈ 𝑌)
219, 20eqeltrrd 2851 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) ∈ 𝑌)
223, 21eqeltrrd 2851 . . . . . 6 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑎 𝑏) ∈ 𝑌)
23 simpr 471 . . . . . . . 8 ((𝑎𝑌𝑏𝑌) → 𝑏𝑌)
24 foelrni 6388 . . . . . . . 8 ((𝐹:𝑋onto𝑌𝑏𝑌) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2510, 23, 24syl2an 583 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2625ad2antrr 705 . . . . . 6 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2722, 26r19.29a 3226 . . . . 5 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 𝑏) ∈ 𝑌)
28 simpl 468 . . . . . 6 ((𝑎𝑌𝑏𝑌) → 𝑎𝑌)
29 foelrni 6388 . . . . . 6 ((𝐹:𝑋onto𝑌𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3010, 28, 29syl2an 583 . . . . 5 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3127, 30r19.29a 3226 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → (𝑎 𝑏) ∈ 𝑌)
32 simpll 750 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝜑)
33 simplrl 762 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑎𝑌)
34 simplrr 763 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑏𝑌)
35 simpr 471 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑐𝑌)
3614ad2antrr 705 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) → 𝐺 ∈ Mnd)
3736ad5antr 716 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝐺 ∈ Mnd)
38 simp-6r 778 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑖𝑋)
39 simp-4r 770 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑗𝑋)
40 simplr 752 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑘𝑋)
4116, 17mndass 17510 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑖𝑋𝑗𝑋𝑘𝑋)) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4237, 38, 39, 40, 41syl13anc 1478 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4342fveq2d 6337 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = (𝐹‘(𝑖 + (𝑗 + 𝑘))))
44 simp-7l 780 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝜑)
4544, 5syl3an1 1166 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
4637, 38, 39, 18syl3anc 1476 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑖 + 𝑗) ∈ 𝑋)
4745, 46, 40mhmlem 17743 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)))
4816, 17mndcl 17509 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑗𝑋𝑘𝑋) → (𝑗 + 𝑘) ∈ 𝑋)
4937, 39, 40, 48syl3anc 1476 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑗 + 𝑘) ∈ 𝑋)
5045, 38, 49mhmlem 17743 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + (𝑗 + 𝑘))) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
5143, 47, 503eqtr3d 2813 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
52 simp1 1130 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋𝑗𝑋) → 𝜑)
5352, 5syl3an1 1166 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋𝑗𝑋) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
54 simp2 1131 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑖𝑋)
55 simp3 1132 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑗𝑋)
5653, 54, 55mhmlem 17743 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋𝑗𝑋) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5744, 38, 39, 56syl3anc 1476 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5857oveq1d 6811 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)))
5945, 39, 40mhmlem 17743 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑗 + 𝑘)) = ((𝐹𝑗) (𝐹𝑘)))
6059oveq2d 6812 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
6151, 58, 603eqtr3d 2813 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
62 simp-5r 774 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑖) = 𝑎)
63 simpllr 760 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑗) = 𝑏)
6462, 63oveq12d 6814 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
65 simpr 471 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑘) = 𝑐)
6664, 65oveq12d 6814 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝑎 𝑏) 𝑐))
6763, 65oveq12d 6814 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑗) (𝐹𝑘)) = (𝑏 𝑐))
6862, 67oveq12d 6814 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))) = (𝑎 (𝑏 𝑐)))
6961, 66, 683eqtr3d 2813 . . . . . . . . 9 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
70 foelrni 6388 . . . . . . . . . . . 12 ((𝐹:𝑋onto𝑌𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7110, 70sylan 569 . . . . . . . . . . 11 ((𝜑𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
72713ad2antr3 1205 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7372ad4antr 712 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7469, 73r19.29a 3226 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
75253adantr3 1176 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7675ad2antrr 705 . . . . . . . 8 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7774, 76r19.29a 3226 . . . . . . 7 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
78303adantr3 1176 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
7977, 78r19.29a 3226 . . . . . 6 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8032, 33, 34, 35, 79syl13anc 1478 . . . . 5 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8180ralrimiva 3115 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8231, 81jca 501 . . 3 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
8382ralrimivva 3120 . 2 (𝜑 → ∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
84 eqid 2771 . . . . . 6 (0g𝐺) = (0g𝐺)
8516, 84mndidcl 17516 . . . . 5 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝑋)
8614, 85syl 17 . . . 4 (𝜑 → (0g𝐺) ∈ 𝑋)
8712, 86ffvelrnd 6505 . . 3 (𝜑 → (𝐹‘(0g𝐺)) ∈ 𝑌)
88 simplll 758 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝜑)
8988, 5syl3an1 1166 . . . . . . . . 9 (((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
9014ad3antrrr 709 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝐺 ∈ Mnd)
9190, 85syl 17 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (0g𝐺) ∈ 𝑋)
92 simplr 752 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝑖𝑋)
9389, 91, 92mhmlem 17743 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = ((𝐹‘(0g𝐺)) (𝐹𝑖)))
9416, 17, 84mndlid 17519 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → ((0g𝐺) + 𝑖) = 𝑖)
9590, 92, 94syl2anc 573 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((0g𝐺) + 𝑖) = 𝑖)
9695fveq2d 6337 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = (𝐹𝑖))
9793, 96eqtr3d 2807 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = (𝐹𝑖))
98 simpr 471 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹𝑖) = 𝑎)
9998oveq2d 6812 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = ((𝐹‘(0g𝐺)) 𝑎))
10097, 99, 983eqtr3d 2813 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) 𝑎) = 𝑎)
10189, 92, 91mhmlem 17743 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = ((𝐹𝑖) (𝐹‘(0g𝐺))))
10216, 17, 84mndrid 17520 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → (𝑖 + (0g𝐺)) = 𝑖)
10390, 92, 102syl2anc 573 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑖 + (0g𝐺)) = 𝑖)
104103fveq2d 6337 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = (𝐹𝑖))
105101, 104eqtr3d 2807 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝐹𝑖))
10698oveq1d 6811 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝑎 (𝐹‘(0g𝐺))))
107105, 106, 983eqtr3d 2813 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 (𝐹‘(0g𝐺))) = 𝑎)
108100, 107jca 501 . . . . 5 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
10910, 29sylan 569 . . . . 5 ((𝜑𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
110108, 109r19.29a 3226 . . . 4 ((𝜑𝑎𝑌) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
111110ralrimiva 3115 . . 3 (𝜑 → ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
112 oveq1 6803 . . . . . 6 (𝑑 = (𝐹‘(0g𝐺)) → (𝑑 𝑎) = ((𝐹‘(0g𝐺)) 𝑎))
113112eqeq1d 2773 . . . . 5 (𝑑 = (𝐹‘(0g𝐺)) → ((𝑑 𝑎) = 𝑎 ↔ ((𝐹‘(0g𝐺)) 𝑎) = 𝑎))
114113ovanraleqv 6820 . . . 4 (𝑑 = (𝐹‘(0g𝐺)) → (∀𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎) ↔ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)))
115114rspcev 3460 . . 3 (((𝐹‘(0g𝐺)) ∈ 𝑌 ∧ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)) → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
11687, 111, 115syl2anc 573 . 2 (𝜑 → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
117 ghmgrp.y . . 3 𝑌 = (Base‘𝐻)
118 ghmgrp.q . . 3 = (+g𝐻)
119117, 118ismnd 17505 . 2 (𝐻 ∈ Mnd ↔ (∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))) ∧ ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎)))
12083, 116, 119sylanbrc 572 1 (𝜑𝐻 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  wrex 3062  wf 6026  ontowfo 6028  cfv 6030  (class class class)co 6796  Basecbs 16064  +gcplusg 16149  0gc0g 16308  Mndcmnd 17502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-fo 6036  df-fv 6038  df-riota 6757  df-ov 6799  df-0g 16310  df-mgm 17450  df-sgrp 17492  df-mnd 17503
This theorem is referenced by:  mhmfmhm  17746  ghmgrp  17747  ghmcmn  18444
  Copyright terms: Public domain W3C validator