Metamath Proof Explorer


Theorem imasmndf1

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

Ref Expression
Hypotheses imasmndf1.u 𝑈 = ( 𝐹s 𝑅 )
imasmndf1.v 𝑉 = ( Base ‘ 𝑅 )
Assertion imasmndf1 ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → 𝑈 ∈ Mnd )

Proof

Step Hyp Ref Expression
1 imasmndf1.u 𝑈 = ( 𝐹s 𝑅 )
2 imasmndf1.v 𝑉 = ( Base ‘ 𝑅 )
3 1 a1i ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → 𝑈 = ( 𝐹s 𝑅 ) )
4 2 a1i ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → 𝑉 = ( Base ‘ 𝑅 ) )
5 eqid ( +g𝑅 ) = ( +g𝑅 )
6 f1f1orn ( 𝐹 : 𝑉1-1𝐵𝐹 : 𝑉1-1-onto→ ran 𝐹 )
7 6 adantr ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → 𝐹 : 𝑉1-1-onto→ ran 𝐹 )
8 f1ofo ( 𝐹 : 𝑉1-1-onto→ ran 𝐹𝐹 : 𝑉onto→ ran 𝐹 )
9 7 8 syl ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → 𝐹 : 𝑉onto→ ran 𝐹 )
10 7 f1ocpbl ( ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) ∧ ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑝𝑉𝑞𝑉 ) ) → ( ( ( 𝐹𝑎 ) = ( 𝐹𝑝 ) ∧ ( 𝐹𝑏 ) = ( 𝐹𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g𝑅 ) 𝑞 ) ) ) )
11 simpr ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → 𝑅 ∈ Mnd )
12 eqid ( 0g𝑅 ) = ( 0g𝑅 )
13 3 4 5 9 10 11 12 imasmnd ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → ( 𝑈 ∈ Mnd ∧ ( 𝐹 ‘ ( 0g𝑅 ) ) = ( 0g𝑈 ) ) )
14 13 simpld ( ( 𝐹 : 𝑉1-1𝐵𝑅 ∈ Mnd ) → 𝑈 ∈ Mnd )