Metamath Proof Explorer

Theorem ghmcmn

Description: The image of a commutative monoid G under a group homomorphism F is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020)

Ref Expression
Hypotheses ghmabl.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
ghmabl.y ⊢ 𝑌 = ( Base ‘ 𝐻 )
ghmabl.p ⊢ + = ( +g ‘ 𝐺 )
ghmabl.q ⊢ ⨣ = ( +g ‘ 𝐻 )
ghmabl.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
ghmabl.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
ghmcmn.3 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
Assertion ghmcmn ( 𝜑 → 𝐻 ∈ CMnd )

Proof

Step Hyp Ref Expression
1 ghmabl.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 ghmabl.y ⊢ 𝑌 = ( Base ‘ 𝐻 )
3 ghmabl.p ⊢ + = ( +g ‘ 𝐺 )
4 ghmabl.q ⊢ ⨣ = ( +g ‘ 𝐻 )
5 ghmabl.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
6 ghmabl.1 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
7 ghmcmn.3 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
8 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
9 7 8 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
10 5 1 2 3 4 6 9 mhmmnd ⊢ ( 𝜑 → 𝐻 ∈ Mnd )
11 simp-6l ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → 𝜑 )
12 11 7 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → 𝐺 ∈ CMnd )
13 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → 𝑎 ∈ 𝑋 )
14 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → 𝑏 ∈ 𝑋 )
15 1 3 cmncom ⊢ ( ( 𝐺 ∈ CMnd ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑎 + 𝑏 ) = ( 𝑏 + 𝑎 ) )
16 12 13 14 15 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( 𝑎 + 𝑏 ) = ( 𝑏 + 𝑎 ) )
17 16 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑏 + 𝑎 ) ) )
18 11 5 syl3an1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
19 18 13 14 mhmlem ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) )
20 18 14 13 mhmlem ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( 𝐹 ‘ ( 𝑏 + 𝑎 ) ) = ( ( 𝐹 ‘ 𝑏 ) ⨣ ( 𝐹 ‘ 𝑎 ) ) )
21 17 19 20 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ⨣ ( 𝐹 ‘ 𝑎 ) ) )
22 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( 𝐹 ‘ 𝑎 ) = 𝑖 )
23 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( 𝐹 ‘ 𝑏 ) = 𝑗 )
24 22 23 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( ( 𝐹 ‘ 𝑎 ) ⨣ ( 𝐹 ‘ 𝑏 ) ) = ( 𝑖 ⨣ 𝑗 ) )
25 23 22 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( ( 𝐹 ‘ 𝑏 ) ⨣ ( 𝐹 ‘ 𝑎 ) ) = ( 𝑗 ⨣ 𝑖 ) )
26 21 24 25 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) ∧ 𝑏 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑏 ) = 𝑗 ) → ( 𝑖 ⨣ 𝑗 ) = ( 𝑗 ⨣ 𝑖 ) )
27 foelcdmi ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑗 ∈ 𝑌 ) → ∃ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑏 ) = 𝑗 )
28 6 27 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑌 ) → ∃ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑏 ) = 𝑗 )
29 28 ad5ant13 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) → ∃ 𝑏 ∈ 𝑋 ( 𝐹 ‘ 𝑏 ) = 𝑗 )
30 26 29 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) ∧ 𝑎 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑖 ) → ( 𝑖 ⨣ 𝑗 ) = ( 𝑗 ⨣ 𝑖 ) )
31 foelcdmi ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑖 ∈ 𝑌 ) → ∃ 𝑎 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) = 𝑖 )
32 6 31 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) → ∃ 𝑎 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) = 𝑖 )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) → ∃ 𝑎 ∈ 𝑋 ( 𝐹 ‘ 𝑎 ) = 𝑖 )
34 30 33 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑌 ) ∧ 𝑗 ∈ 𝑌 ) → ( 𝑖 ⨣ 𝑗 ) = ( 𝑗 ⨣ 𝑖 ) )
35 34 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑌 ∧ 𝑗 ∈ 𝑌 ) ) → ( 𝑖 ⨣ 𝑗 ) = ( 𝑗 ⨣ 𝑖 ) )
36 35 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑌 ∀ 𝑗 ∈ 𝑌 ( 𝑖 ⨣ 𝑗 ) = ( 𝑗 ⨣ 𝑖 ) )
37 2 4 iscmn ⊢ ( 𝐻 ∈ CMnd ↔ ( 𝐻 ∈ Mnd ∧ ∀ 𝑖 ∈ 𝑌 ∀ 𝑗 ∈ 𝑌 ( 𝑖 ⨣ 𝑗 ) = ( 𝑗 ⨣ 𝑖 ) ) )
38 10 36 37 sylanbrc ⊢ ( 𝜑 → 𝐻 ∈ CMnd )