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

Theorem mhmmnd 17584
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 815 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑖) = 𝑎)
2 simpr 476 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑗) = 𝑏)
31, 2oveq12d 6708 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
4 simp-5l 825 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝜑)
5 ghmgrp.f . . . . . . . . . 10 ((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
64, 5syl3an1 1399 . . . . . . . . 9 (((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
7 simp-4r 824 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑖𝑋)
8 simplr 807 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑗𝑋)
96, 7, 8mhmlem 17582 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
10 ghmgrp.1 . . . . . . . . . . 11 (𝜑𝐹:𝑋onto𝑌)
11 fof 6153 . . . . . . . . . . 11 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
1210, 11syl 17 . . . . . . . . . 10 (𝜑𝐹:𝑋𝑌)
1312ad5antr 773 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐹:𝑋𝑌)
14 mhmmnd.3 . . . . . . . . . . 11 (𝜑𝐺 ∈ Mnd)
1514ad5antr 773 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐺 ∈ Mnd)
16 ghmgrp.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
17 ghmgrp.p . . . . . . . . . . 11 + = (+g𝐺)
1816, 17mndcl 17348 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋𝑗𝑋) → (𝑖 + 𝑗) ∈ 𝑋)
1915, 7, 8, 18syl3anc 1366 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑖 + 𝑗) ∈ 𝑋)
2013, 19ffvelrnd 6400 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) ∈ 𝑌)
219, 20eqeltrrd 2731 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) ∈ 𝑌)
223, 21eqeltrrd 2731 . . . . . 6 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑎 𝑏) ∈ 𝑌)
23 simpr 476 . . . . . . . 8 ((𝑎𝑌𝑏𝑌) → 𝑏𝑌)
24 foelrni 6283 . . . . . . . 8 ((𝐹:𝑋onto𝑌𝑏𝑌) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2510, 23, 24syl2an 493 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2625ad2antrr 762 . . . . . 6 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2722, 26r19.29a 3107 . . . . 5 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 𝑏) ∈ 𝑌)
28 simpl 472 . . . . . 6 ((𝑎𝑌𝑏𝑌) → 𝑎𝑌)
29 foelrni 6283 . . . . . 6 ((𝐹:𝑋onto𝑌𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3010, 28, 29syl2an 493 . . . . 5 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3127, 30r19.29a 3107 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → (𝑎 𝑏) ∈ 𝑌)
32 simpll 805 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝜑)
33 simplrl 817 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑎𝑌)
34 simplrr 818 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑏𝑌)
35 simpr 476 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑐𝑌)
3614ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) → 𝐺 ∈ Mnd)
3736ad5antr 773 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝐺 ∈ Mnd)
38 simp-6r 828 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑖𝑋)
39 simp-4r 824 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑗𝑋)
40 simplr 807 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑘𝑋)
4116, 17mndass 17349 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑖𝑋𝑗𝑋𝑘𝑋)) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4237, 38, 39, 40, 41syl13anc 1368 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4342fveq2d 6233 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = (𝐹‘(𝑖 + (𝑗 + 𝑘))))
44 simp-7l 829 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝜑)
4544, 5syl3an1 1399 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
4637, 38, 39, 18syl3anc 1366 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑖 + 𝑗) ∈ 𝑋)
4745, 46, 40mhmlem 17582 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)))
4816, 17mndcl 17348 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑗𝑋𝑘𝑋) → (𝑗 + 𝑘) ∈ 𝑋)
4937, 39, 40, 48syl3anc 1366 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑗 + 𝑘) ∈ 𝑋)
5045, 38, 49mhmlem 17582 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + (𝑗 + 𝑘))) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
5143, 47, 503eqtr3d 2693 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
52 simp1 1081 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋𝑗𝑋) → 𝜑)
5352, 5syl3an1 1399 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋𝑗𝑋) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
54 simp2 1082 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑖𝑋)
55 simp3 1083 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑗𝑋)
5653, 54, 55mhmlem 17582 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋𝑗𝑋) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5744, 38, 39, 56syl3anc 1366 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5857oveq1d 6705 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)))
5945, 39, 40mhmlem 17582 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑗 + 𝑘)) = ((𝐹𝑗) (𝐹𝑘)))
6059oveq2d 6706 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
6151, 58, 603eqtr3d 2693 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
62 simp-5r 826 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑖) = 𝑎)
63 simpllr 815 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑗) = 𝑏)
6462, 63oveq12d 6708 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
65 simpr 476 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑘) = 𝑐)
6664, 65oveq12d 6708 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝑎 𝑏) 𝑐))
6763, 65oveq12d 6708 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑗) (𝐹𝑘)) = (𝑏 𝑐))
6862, 67oveq12d 6708 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))) = (𝑎 (𝑏 𝑐)))
6961, 66, 683eqtr3d 2693 . . . . . . . . 9 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
70 foelrni 6283 . . . . . . . . . . . 12 ((𝐹:𝑋onto𝑌𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7110, 70sylan 487 . . . . . . . . . . 11 ((𝜑𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
72713ad2antr3 1248 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7372ad4antr 769 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7469, 73r19.29a 3107 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
75253adantr3 1242 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7675ad2antrr 762 . . . . . . . 8 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7774, 76r19.29a 3107 . . . . . . 7 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
78303adantr3 1242 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
7977, 78r19.29a 3107 . . . . . 6 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8032, 33, 34, 35, 79syl13anc 1368 . . . . 5 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8180ralrimiva 2995 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8231, 81jca 553 . . 3 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
8382ralrimivva 3000 . 2 (𝜑 → ∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
84 eqid 2651 . . . . . 6 (0g𝐺) = (0g𝐺)
8516, 84mndidcl 17355 . . . . 5 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝑋)
8614, 85syl 17 . . . 4 (𝜑 → (0g𝐺) ∈ 𝑋)
8712, 86ffvelrnd 6400 . . 3 (𝜑 → (𝐹‘(0g𝐺)) ∈ 𝑌)
88 simplll 813 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝜑)
8988, 5syl3an1 1399 . . . . . . . . 9 (((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
9014ad3antrrr 766 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝐺 ∈ Mnd)
9190, 85syl 17 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (0g𝐺) ∈ 𝑋)
92 simplr 807 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝑖𝑋)
9389, 91, 92mhmlem 17582 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = ((𝐹‘(0g𝐺)) (𝐹𝑖)))
9416, 17, 84mndlid 17358 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → ((0g𝐺) + 𝑖) = 𝑖)
9590, 92, 94syl2anc 694 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((0g𝐺) + 𝑖) = 𝑖)
9695fveq2d 6233 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = (𝐹𝑖))
9793, 96eqtr3d 2687 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = (𝐹𝑖))
98 simpr 476 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹𝑖) = 𝑎)
9998oveq2d 6706 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = ((𝐹‘(0g𝐺)) 𝑎))
10097, 99, 983eqtr3d 2693 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) 𝑎) = 𝑎)
10189, 92, 91mhmlem 17582 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = ((𝐹𝑖) (𝐹‘(0g𝐺))))
10216, 17, 84mndrid 17359 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → (𝑖 + (0g𝐺)) = 𝑖)
10390, 92, 102syl2anc 694 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑖 + (0g𝐺)) = 𝑖)
104103fveq2d 6233 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = (𝐹𝑖))
105101, 104eqtr3d 2687 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝐹𝑖))
10698oveq1d 6705 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝑎 (𝐹‘(0g𝐺))))
107105, 106, 983eqtr3d 2693 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 (𝐹‘(0g𝐺))) = 𝑎)
108100, 107jca 553 . . . . 5 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
10910, 29sylan 487 . . . . 5 ((𝜑𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
110108, 109r19.29a 3107 . . . 4 ((𝜑𝑎𝑌) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
111110ralrimiva 2995 . . 3 (𝜑 → ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
112 oveq1 6697 . . . . . . 7 (𝑑 = (𝐹‘(0g𝐺)) → (𝑑 𝑎) = ((𝐹‘(0g𝐺)) 𝑎))
113112eqeq1d 2653 . . . . . 6 (𝑑 = (𝐹‘(0g𝐺)) → ((𝑑 𝑎) = 𝑎 ↔ ((𝐹‘(0g𝐺)) 𝑎) = 𝑎))
114 oveq2 6698 . . . . . . 7 (𝑑 = (𝐹‘(0g𝐺)) → (𝑎 𝑑) = (𝑎 (𝐹‘(0g𝐺))))
115114eqeq1d 2653 . . . . . 6 (𝑑 = (𝐹‘(0g𝐺)) → ((𝑎 𝑑) = 𝑎 ↔ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
116113, 115anbi12d 747 . . . . 5 (𝑑 = (𝐹‘(0g𝐺)) → (((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎) ↔ (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)))
117116ralbidv 3015 . . . 4 (𝑑 = (𝐹‘(0g𝐺)) → (∀𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎) ↔ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)))
118117rspcev 3340 . . 3 (((𝐹‘(0g𝐺)) ∈ 𝑌 ∧ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)) → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
11987, 111, 118syl2anc 694 . 2 (𝜑 → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
120 ghmgrp.y . . 3 𝑌 = (Base‘𝐻)
121 ghmgrp.q . . 3 = (+g𝐻)
122120, 121ismnd 17344 . 2 (𝐻 ∈ Mnd ↔ (∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))) ∧ ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎)))
12383, 119, 122sylanbrc 699 1 (𝜑𝐻 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  wf 5922  ontowfo 5924  cfv 5926  (class class class)co 6690  Basecbs 15904  +gcplusg 15988  0gc0g 16147  Mndcmnd 17341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fo 5932  df-fv 5934  df-riota 6651  df-ov 6693  df-0g 16149  df-mgm 17289  df-sgrp 17331  df-mnd 17342
This theorem is referenced by:  mhmfmhm  17585  ghmgrp  17586  ghmcmn  18283
  Copyright terms: Public domain W3C validator