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 )