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

Theorem mhmmnd 18869
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 774 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑖) = 𝑎)
2 simpr 485 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹𝑗) = 𝑏)
31, 2oveq12d 7375 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
4 simp-5l 783 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝜑)
5 ghmgrp.f . . . . . . . . . 10 ((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
64, 5syl3an1 1163 . . . . . . . . 9 (((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
7 simp-4r 782 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑖𝑋)
8 simplr 767 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝑗𝑋)
96, 7, 8mhmlem 18867 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
10 ghmgrp.1 . . . . . . . . . . 11 (𝜑𝐹:𝑋onto𝑌)
11 fof 6756 . . . . . . . . . . 11 (𝐹:𝑋onto𝑌𝐹:𝑋𝑌)
1210, 11syl 17 . . . . . . . . . 10 (𝜑𝐹:𝑋𝑌)
1312ad5antr 732 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐹:𝑋𝑌)
14 mhmmnd.3 . . . . . . . . . . 11 (𝜑𝐺 ∈ Mnd)
1514ad5antr 732 . . . . . . . . . 10 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → 𝐺 ∈ Mnd)
16 ghmgrp.x . . . . . . . . . . 11 𝑋 = (Base‘𝐺)
17 ghmgrp.p . . . . . . . . . . 11 + = (+g𝐺)
1816, 17mndcl 18564 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋𝑗𝑋) → (𝑖 + 𝑗) ∈ 𝑋)
1915, 7, 8, 18syl3anc 1371 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑖 + 𝑗) ∈ 𝑋)
2013, 19ffvelcdmd 7036 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝐹‘(𝑖 + 𝑗)) ∈ 𝑌)
219, 20eqeltrrd 2839 . . . . . . 7 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝐹𝑖) (𝐹𝑗)) ∈ 𝑌)
223, 21eqeltrrd 2839 . . . . . 6 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → (𝑎 𝑏) ∈ 𝑌)
23 simpr 485 . . . . . . . 8 ((𝑎𝑌𝑏𝑌) → 𝑏𝑌)
24 foelcdmi 6904 . . . . . . . 8 ((𝐹:𝑋onto𝑌𝑏𝑌) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2510, 23, 24syl2an 596 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2625ad2antrr 724 . . . . . 6 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
2722, 26r19.29a 3159 . . . . 5 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 𝑏) ∈ 𝑌)
28 simpl 483 . . . . . 6 ((𝑎𝑌𝑏𝑌) → 𝑎𝑌)
29 foelcdmi 6904 . . . . . 6 ((𝐹:𝑋onto𝑌𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3010, 28, 29syl2an 596 . . . . 5 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
3127, 30r19.29a 3159 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → (𝑎 𝑏) ∈ 𝑌)
32 simpll 765 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝜑)
33 simplrl 775 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑎𝑌)
34 simplrr 776 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑏𝑌)
35 simpr 485 . . . . . 6 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → 𝑐𝑌)
3614ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) → 𝐺 ∈ Mnd)
3736ad5antr 732 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝐺 ∈ Mnd)
38 simp-6r 786 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑖𝑋)
39 simp-4r 782 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑗𝑋)
40 simplr 767 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝑘𝑋)
4116, 17mndass 18565 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ (𝑖𝑋𝑗𝑋𝑘𝑋)) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4237, 38, 39, 40, 41syl13anc 1372 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑖 + 𝑗) + 𝑘) = (𝑖 + (𝑗 + 𝑘)))
4342fveq2d 6846 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = (𝐹‘(𝑖 + (𝑗 + 𝑘))))
44 simp-7l 787 . . . . . . . . . . . . . 14 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → 𝜑)
4544, 5syl3an1 1163 . . . . . . . . . . . . 13 (((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
4637, 38, 39, 18syl3anc 1371 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑖 + 𝑗) ∈ 𝑋)
4745, 46, 40mhmlem 18867 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘((𝑖 + 𝑗) + 𝑘)) = ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)))
4816, 17mndcl 18564 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑗𝑋𝑘𝑋) → (𝑗 + 𝑘) ∈ 𝑋)
4937, 39, 40, 48syl3anc 1371 . . . . . . . . . . . . 13 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝑗 + 𝑘) ∈ 𝑋)
5045, 38, 49mhmlem 18867 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + (𝑗 + 𝑘))) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
5143, 47, 503eqtr3d 2784 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))))
52 simp1 1136 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋𝑗𝑋) → 𝜑)
5352, 5syl3an1 1163 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋𝑗𝑋) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
54 simp2 1137 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑖𝑋)
55 simp3 1138 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋𝑗𝑋) → 𝑗𝑋)
5653, 54, 55mhmlem 18867 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋𝑗𝑋) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5744, 38, 39, 56syl3anc 1371 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑖 + 𝑗)) = ((𝐹𝑖) (𝐹𝑗)))
5857oveq1d 7372 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹‘(𝑖 + 𝑗)) (𝐹𝑘)) = (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)))
5945, 39, 40mhmlem 18867 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹‘(𝑗 + 𝑘)) = ((𝐹𝑗) (𝐹𝑘)))
6059oveq2d 7373 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹‘(𝑗 + 𝑘))) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
6151, 58, 603eqtr3d 2784 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))))
62 simp-5r 784 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑖) = 𝑎)
63 simpllr 774 . . . . . . . . . . . 12 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑗) = 𝑏)
6462, 63oveq12d 7375 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) (𝐹𝑗)) = (𝑎 𝑏))
65 simpr 485 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (𝐹𝑘) = 𝑐)
6664, 65oveq12d 7375 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → (((𝐹𝑖) (𝐹𝑗)) (𝐹𝑘)) = ((𝑎 𝑏) 𝑐))
6763, 65oveq12d 7375 . . . . . . . . . . 11 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑗) (𝐹𝑘)) = (𝑏 𝑐))
6862, 67oveq12d 7375 . . . . . . . . . 10 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝐹𝑖) ((𝐹𝑗) (𝐹𝑘))) = (𝑎 (𝑏 𝑐)))
6961, 66, 683eqtr3d 2784 . . . . . . . . 9 ((((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) ∧ 𝑘𝑋) ∧ (𝐹𝑘) = 𝑐) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
70 foelcdmi 6904 . . . . . . . . . . . 12 ((𝐹:𝑋onto𝑌𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7110, 70sylan 580 . . . . . . . . . . 11 ((𝜑𝑐𝑌) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
72713ad2antr3 1190 . . . . . . . . . 10 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7372ad4antr 730 . . . . . . . . 9 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ∃𝑘𝑋 (𝐹𝑘) = 𝑐)
7469, 73r19.29a 3159 . . . . . . . 8 ((((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑗𝑋) ∧ (𝐹𝑗) = 𝑏) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
75253adantr3 1171 . . . . . . . . 9 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7675ad2antrr 724 . . . . . . . 8 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ∃𝑗𝑋 (𝐹𝑗) = 𝑏)
7774, 76r19.29a 3159 . . . . . . 7 ((((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
78303adantr3 1171 . . . . . . 7 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
7977, 78r19.29a 3159 . . . . . 6 ((𝜑 ∧ (𝑎𝑌𝑏𝑌𝑐𝑌)) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8032, 33, 34, 35, 79syl13anc 1372 . . . . 5 (((𝜑 ∧ (𝑎𝑌𝑏𝑌)) ∧ 𝑐𝑌) → ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8180ralrimiva 3143 . . . 4 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐)))
8231, 81jca 512 . . 3 ((𝜑 ∧ (𝑎𝑌𝑏𝑌)) → ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
8382ralrimivva 3197 . 2 (𝜑 → ∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))))
84 eqid 2736 . . . . . 6 (0g𝐺) = (0g𝐺)
8516, 84mndidcl 18571 . . . . 5 (𝐺 ∈ Mnd → (0g𝐺) ∈ 𝑋)
8614, 85syl 17 . . . 4 (𝜑 → (0g𝐺) ∈ 𝑋)
8712, 86ffvelcdmd 7036 . . 3 (𝜑 → (𝐹‘(0g𝐺)) ∈ 𝑌)
88 simplll 773 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝜑)
8988, 5syl3an1 1163 . . . . . . . . 9 (((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) ∧ 𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))
9014ad3antrrr 728 . . . . . . . . . 10 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝐺 ∈ Mnd)
9190, 85syl 17 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (0g𝐺) ∈ 𝑋)
92 simplr 767 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → 𝑖𝑋)
9389, 91, 92mhmlem 18867 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = ((𝐹‘(0g𝐺)) (𝐹𝑖)))
9416, 17, 84mndlid 18576 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → ((0g𝐺) + 𝑖) = 𝑖)
9590, 92, 94syl2anc 584 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((0g𝐺) + 𝑖) = 𝑖)
9695fveq2d 6846 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘((0g𝐺) + 𝑖)) = (𝐹𝑖))
9793, 96eqtr3d 2778 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = (𝐹𝑖))
98 simpr 485 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹𝑖) = 𝑎)
9998oveq2d 7373 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) (𝐹𝑖)) = ((𝐹‘(0g𝐺)) 𝑎))
10097, 99, 983eqtr3d 2784 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹‘(0g𝐺)) 𝑎) = 𝑎)
10189, 92, 91mhmlem 18867 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = ((𝐹𝑖) (𝐹‘(0g𝐺))))
10216, 17, 84mndrid 18577 . . . . . . . . . 10 ((𝐺 ∈ Mnd ∧ 𝑖𝑋) → (𝑖 + (0g𝐺)) = 𝑖)
10390, 92, 102syl2anc 584 . . . . . . . . 9 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑖 + (0g𝐺)) = 𝑖)
104103fveq2d 6846 . . . . . . . 8 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝐹‘(𝑖 + (0g𝐺))) = (𝐹𝑖))
105101, 104eqtr3d 2778 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝐹𝑖))
10698oveq1d 7372 . . . . . . 7 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → ((𝐹𝑖) (𝐹‘(0g𝐺))) = (𝑎 (𝐹‘(0g𝐺))))
107105, 106, 983eqtr3d 2784 . . . . . 6 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (𝑎 (𝐹‘(0g𝐺))) = 𝑎)
108100, 107jca 512 . . . . 5 ((((𝜑𝑎𝑌) ∧ 𝑖𝑋) ∧ (𝐹𝑖) = 𝑎) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
10910, 29sylan 580 . . . . 5 ((𝜑𝑎𝑌) → ∃𝑖𝑋 (𝐹𝑖) = 𝑎)
110108, 109r19.29a 3159 . . . 4 ((𝜑𝑎𝑌) → (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
111110ralrimiva 3143 . . 3 (𝜑 → ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎))
112 oveq1 7364 . . . . . 6 (𝑑 = (𝐹‘(0g𝐺)) → (𝑑 𝑎) = ((𝐹‘(0g𝐺)) 𝑎))
113112eqeq1d 2738 . . . . 5 (𝑑 = (𝐹‘(0g𝐺)) → ((𝑑 𝑎) = 𝑎 ↔ ((𝐹‘(0g𝐺)) 𝑎) = 𝑎))
114113ovanraleqv 7381 . . . 4 (𝑑 = (𝐹‘(0g𝐺)) → (∀𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎) ↔ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)))
115114rspcev 3581 . . 3 (((𝐹‘(0g𝐺)) ∈ 𝑌 ∧ ∀𝑎𝑌 (((𝐹‘(0g𝐺)) 𝑎) = 𝑎 ∧ (𝑎 (𝐹‘(0g𝐺))) = 𝑎)) → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
11687, 111, 115syl2anc 584 . 2 (𝜑 → ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎))
117 ghmgrp.y . . 3 𝑌 = (Base‘𝐻)
118 ghmgrp.q . . 3 = (+g𝐻)
119117, 118ismnd 18559 . 2 (𝐻 ∈ Mnd ↔ (∀𝑎𝑌𝑏𝑌 ((𝑎 𝑏) ∈ 𝑌 ∧ ∀𝑐𝑌 ((𝑎 𝑏) 𝑐) = (𝑎 (𝑏 𝑐))) ∧ ∃𝑑𝑌𝑎𝑌 ((𝑑 𝑎) = 𝑎 ∧ (𝑎 𝑑) = 𝑎)))
12083, 116, 119sylanbrc 583 1 (𝜑𝐻 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  wf 6492  ontowfo 6494  cfv 6496  (class class class)co 7357  Basecbs 17083  +gcplusg 17133  0gc0g 17321  Mndcmnd 18556
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fo 6502  df-fv 6504  df-riota 7313  df-ov 7360  df-0g 17323  df-mgm 18497  df-sgrp 18546  df-mnd 18557
This theorem is referenced by:  mhmfmhm  18870  ghmgrp  18871  ghmcmn  19610
  Copyright terms: Public domain W3C validator