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 ⊢ U = F “ 𝑠 R
imasmndf1.v ⊢ V = Base R
Assertion imasmndf1 ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → U ∈ Mnd

Proof

Step Hyp Ref Expression
1 imasmndf1.u ⊢ U = F “ 𝑠 R
2 imasmndf1.v ⊢ V = Base R
3 1 a1i ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → U = F “ 𝑠 R
4 2 a1i ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → V = Base R
5 eqid ⊢ + R = + R
6 f1f1orn ⊢ F : V ⟶ 1-1 B → F : V ⟶ 1-1 onto ran ⁡ F
7 6 adantr ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → F : V ⟶ 1-1 onto ran ⁡ F
8 f1ofo ⊢ F : V ⟶ 1-1 onto ran ⁡ F → F : V ⟶ onto ran ⁡ F
9 7 8 syl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → F : V ⟶ onto ran ⁡ F
10 7 f1ocpbl ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd ∧ a ∈ V ∧ b ∈ V ∧ p ∈ V ∧ q ∈ V → F ⁡ a = F ⁡ p ∧ F ⁡ b = F ⁡ q → F ⁡ a + R b = F ⁡ p + R q
11 simpr ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → R ∈ Mnd
12 eqid ⊢ 0 R = 0 R
13 3 4 5 9 10 11 12 imasmnd ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → U ∈ Mnd ∧ F ⁡ 0 R = 0 U
14 13 simpld ⊢ F : V ⟶ 1-1 B ∧ R ∈ Mnd → U ∈ Mnd