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

Theorem mhmmnd 18641
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 772 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑖) = 𝑎)
2 simpr 484 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑗) = 𝑏)
31, 2oveq12d 7278 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
4 simp-5l 781 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝜑)
5 ghmgrp.f . . . . . . . . . 10 ((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
64, 5syl3an1 1161 . . . . . . . . 9 (((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
7 simp-4r 780 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑖𝑋)
8 simplr 765 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑗𝑋)
96, 7, 8mhmlem 18639 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
10 ghmgrp.1 . . . . . . . . . . 11 (𝜑𝐹:𝑋onto𝑌)
11 fof 6677 . . . . . . . . . . 11 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
1210, 11syl 17 . . . . . . . . . 10 (𝜑𝐹:𝑋𝑌)
1312ad5antr 730 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐹:𝑋𝑌)
14 mhmmnd.3 . . . . . . . . . . 11 (𝜑𝐺 ∈ Mnd)
1514ad5antr 730 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐺 ∈ Mnd)
16 ghmgrp.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
17 ghmgrp.p . . . . . . . . . . 11 + = (+g𝐺)
1816, 17mndcl 18337 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋𝑗𝑋) → (𝑖 + 𝑗) ∈ 𝑋)
1915, 7, 8, 18syl3anc 1369 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑖 + 𝑗) ∈ 𝑋)
2013, 19ffvelrnd 6949 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) ∈ 𝑌)
219, 20eqeltrrd 2838 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) ∈ 𝑌)
223, 21eqeltrrd 2838 . . . . . 6 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑎 𝑏) ∈ 𝑌)
23 simpr 484 . . . . . . . 8 ((𝑎𝑌𝑏𝑌) → 𝑏𝑌)
24 foelrni 6818 . . . . . . . 8 ((𝐹:𝑋onto𝑌𝑏𝑌) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2510, 23, 24syl2an 595 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2625ad2antrr 722 . . . . . 6 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2722, 26r19.29a 3216 . . . . 5 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 𝑏) ∈ 𝑌)
28 simpl 482 . . . . . 6 ((𝑎𝑌𝑏𝑌) → 𝑎𝑌)
29 foelrni 6818 . . . . . 6 ((𝐹:𝑋onto𝑌𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3010, 28, 29syl2an 595 . . . . 5 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3127, 30r19.29a 3216 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → (𝑎 𝑏) ∈ 𝑌)
32 simpll 763 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝜑)
33 simplrl 773 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑎𝑌)
34 simplrr 774 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑏𝑌)
35 simpr 484 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑐𝑌)
3614ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) → 𝐺 ∈ Mnd)
3736ad5antr 730 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝐺 ∈ Mnd)
38 simp-6r 784 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑖𝑋)
39 simp-4r 780 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑗𝑋)
40 simplr 765 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑘𝑋)
4116, 17mndass 18338 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑖𝑋𝑗𝑋𝑘𝑋)) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4237, 38, 39, 40, 41syl13anc 1370 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4342fveq2d 6765 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = (𝐹‘(𝑖 + (𝑗 + 𝑘))))
44 simp-7l 785 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝜑)
4544, 5syl3an1 1161 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
4637, 38, 39, 18syl3anc 1369 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑖 + 𝑗) ∈ 𝑋)
4745, 46, 40mhmlem 18639 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)))
4816, 17mndcl 18337 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑗𝑋𝑘𝑋) → (𝑗 + 𝑘) ∈ 𝑋)
4937, 39, 40, 48syl3anc 1369 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑗 + 𝑘) ∈ 𝑋)
5045, 38, 49mhmlem 18639 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + (𝑗 + 𝑘))) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
5143, 47, 503eqtr3d 2785 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
52 simp1 1134 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋𝑗𝑋) → 𝜑)
5352, 5syl3an1 1161 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋𝑗𝑋) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
54 simp2 1135 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑖𝑋)
55 simp3 1136 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑗𝑋)
5653, 54, 55mhmlem 18639 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋𝑗𝑋) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5744, 38, 39, 56syl3anc 1369 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5857oveq1d 7275 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)))
5945, 39, 40mhmlem 18639 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑗 + 𝑘)) = ((𝐹𝑗) (𝐹𝑘)))
6059oveq2d 7276 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
6151, 58, 603eqtr3d 2785 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
62 simp-5r 782 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑖) = 𝑎)
63 simpllr 772 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑗) = 𝑏)
6462, 63oveq12d 7278 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
65 simpr 484 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑘) = 𝑐)
6664, 65oveq12d 7278 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝑎 𝑏) 𝑐))
6763, 65oveq12d 7278 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑗) (𝐹𝑘)) = (𝑏 𝑐))
6862, 67oveq12d 7278 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))) = (𝑎 (𝑏 𝑐)))
6961, 66, 683eqtr3d 2785 . . . . . . . . 9 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
70 foelrni 6818 . . . . . . . . . . . 12 ((𝐹:𝑋onto𝑌𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7110, 70sylan 579 . . . . . . . . . . 11 ((𝜑𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
72713ad2antr3 1188 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7372ad4antr 728 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7469, 73r19.29a 3216 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
75253adantr3 1169 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7675ad2antrr 722 . . . . . . . 8 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7774, 76r19.29a 3216 . . . . . . 7 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
78303adantr3 1169 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
7977, 78r19.29a 3216 . . . . . 6 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8032, 33, 34, 35, 79syl13anc 1370 . . . . 5 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8180ralrimiva 3106 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8231, 81jca 511 . . 3 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
8382ralrimivva 3113 . 2 (𝜑 → ∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
84 eqid 2737 . . . . . 6 (0g𝐺) = (0g𝐺)
8516, 84mndidcl 18344 . . . . 5 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝑋)
8614, 85syl 17 . . . 4 (𝜑 → (0g𝐺) ∈ 𝑋)
8712, 86ffvelrnd 6949 . . 3 (𝜑 → (𝐹‘(0g𝐺)) ∈ 𝑌)
88 simplll 771 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝜑)
8988, 5syl3an1 1161 . . . . . . . . 9 (((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
9014ad3antrrr 726 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝐺 ∈ Mnd)
9190, 85syl 17 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (0g𝐺) ∈ 𝑋)
92 simplr 765 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝑖𝑋)
9389, 91, 92mhmlem 18639 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = ((𝐹‘(0g𝐺)) (𝐹𝑖)))
9416, 17, 84mndlid 18349 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → ((0g𝐺) + 𝑖) = 𝑖)
9590, 92, 94syl2anc 583 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((0g𝐺) + 𝑖) = 𝑖)
9695fveq2d 6765 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = (𝐹𝑖))
9793, 96eqtr3d 2779 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = (𝐹𝑖))
98 simpr 484 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹𝑖) = 𝑎)
9998oveq2d 7276 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = ((𝐹‘(0g𝐺)) 𝑎))
10097, 99, 983eqtr3d 2785 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) 𝑎) = 𝑎)
10189, 92, 91mhmlem 18639 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = ((𝐹𝑖) (𝐹‘(0g𝐺))))
10216, 17, 84mndrid 18350 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → (𝑖 + (0g𝐺)) = 𝑖)
10390, 92, 102syl2anc 583 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑖 + (0g𝐺)) = 𝑖)
104103fveq2d 6765 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = (𝐹𝑖))
105101, 104eqtr3d 2779 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝐹𝑖))
10698oveq1d 7275 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝑎 (𝐹‘(0g𝐺))))
107105, 106, 983eqtr3d 2785 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 (𝐹‘(0g𝐺))) = 𝑎)
108100, 107jca 511 . . . . 5 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
10910, 29sylan 579 . . . . 5 ((𝜑𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
110108, 109r19.29a 3216 . . . 4 ((𝜑𝑎𝑌) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
111110ralrimiva 3106 . . 3 (𝜑 → ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
112 oveq1 7267 . . . . . 6 (𝑑 = (𝐹‘(0g𝐺)) → (𝑑 𝑎) = ((𝐹‘(0g𝐺)) 𝑎))
113112eqeq1d 2739 . . . . 5 (𝑑 = (𝐹‘(0g𝐺)) → ((𝑑 𝑎) = 𝑎 ↔ ((𝐹‘(0g𝐺)) 𝑎) = 𝑎))
114113ovanraleqv 7284 . . . 4 (𝑑 = (𝐹‘(0g𝐺)) → (∀𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎) ↔ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)))
115114rspcev 3557 . . 3 (((𝐹‘(0g𝐺)) ∈ 𝑌 ∧ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)) → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
11687, 111, 115syl2anc 583 . 2 (𝜑 → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
117 ghmgrp.y . . 3 𝑌 = (Base‘𝐻)
118 ghmgrp.q . . 3 = (+g𝐻)
119117, 118ismnd 18332 . 2 (𝐻 ∈ Mnd ↔ (∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))) ∧ ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎)))
12083, 116, 119sylanbrc 582 1 (𝜑𝐻 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085   = wceq 1539  wcel 2107  wral 3062  wrex 3063  wf 6419  ontowfo 6421  cfv 6423  (class class class)co 7260  Basecbs 16856  +gcplusg 16906  0gc0g 17094  Mndcmnd 18329
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3429  df-sbc 3717  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-fo 6429  df-fv 6431  df-riota 7217  df-ov 7263  df-0g 17096  df-mgm 18270  df-sgrp 18319  df-mnd 18330
This theorem is referenced by:  mhmfmhm  18642  ghmgrp  18643  ghmcmn  19377
  Copyright terms: Public domain W3C validator