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 ) |