Metamath Proof Explorer


Theorem imasmnd

Description: The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasmnd.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
imasmnd.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
imasmnd.p + = ( +g𝑅 )
imasmnd.f ( 𝜑𝐹 : 𝑉onto𝐵 )
imasmnd.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasmnd.r ( 𝜑𝑅 ∈ Mnd )
imasmnd.z 0 = ( 0g𝑅 )
Assertion imasmnd ( 𝜑 → ( 𝑈 ∈ Mnd ∧ ( 𝐹0 ) = ( 0g𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 imasmnd.u ( 𝜑𝑈 = ( 𝐹s 𝑅 ) )
2 imasmnd.v ( 𝜑𝑉 = ( Base ‘ 𝑅 ) )
3 imasmnd.p + = ( +g𝑅 )
4 imasmnd.f ( 𝜑𝐹 : 𝑉onto𝐵 )
5 imasmnd.e ( ( 𝜑 ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
6 imasmnd.r ( 𝜑𝑅 ∈ Mnd )
7 imasmnd.z 0 = ( 0g𝑅 )
8 6 3ad2ant1 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑅 ∈ Mnd )
9 simp2 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑥𝑉 )
10 2 3ad2ant1 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑉 = ( Base ‘ 𝑅 ) )
11 9 10 eleqtrd ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
12 simp3 ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑦𝑉 )
13 12 10 eleqtrd ( ( 𝜑𝑥𝑉𝑦𝑉 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
14 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15 14 3 mndcl ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
16 8 11 13 15 syl3anc ( ( 𝜑𝑥𝑉𝑦𝑉 ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
17 16 10 eleqtrrd ( ( 𝜑𝑥𝑉𝑦𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
18 6 adantr ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑅 ∈ Mnd )
19 11 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
20 13 3adant3r3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
21 simpr3 ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑧𝑉 )
22 2 adantr ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
23 21 22 eleqtrd ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
24 14 3 mndass ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
25 18 19 20 23 24 syl13anc ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
26 25 fveq2d ( ( 𝜑 ∧ ( 𝑥𝑉𝑦𝑉𝑧𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
27 14 7 mndidcl ( 𝑅 ∈ Mnd → 0 ∈ ( Base ‘ 𝑅 ) )
28 6 27 syl ( 𝜑0 ∈ ( Base ‘ 𝑅 ) )
29 28 2 eleqtrrd ( 𝜑0𝑉 )
30 2 eleq2d ( 𝜑 → ( 𝑥𝑉𝑥 ∈ ( Base ‘ 𝑅 ) ) )
31 30 biimpa ( ( 𝜑𝑥𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
32 14 3 7 mndlid ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 0 + 𝑥 ) = 𝑥 )
33 6 31 32 syl2an2r ( ( 𝜑𝑥𝑉 ) → ( 0 + 𝑥 ) = 𝑥 )
34 33 fveq2d ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹𝑥 ) )
35 14 3 7 mndrid ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 + 0 ) = 𝑥 )
36 6 31 35 syl2an2r ( ( 𝜑𝑥𝑉 ) → ( 𝑥 + 0 ) = 𝑥 )
37 36 fveq2d ( ( 𝜑𝑥𝑉 ) → ( 𝐹 ‘ ( 𝑥 + 0 ) ) = ( 𝐹𝑥 ) )
38 1 2 3 4 5 6 17 26 29 34 37 imasmnd2 ( 𝜑 → ( 𝑈 ∈ Mnd ∧ ( 𝐹0 ) = ( 0g𝑈 ) ) )