Step |
Hyp |
Ref |
Expression |
1 |
|
imasmndf1.u |
|- U = ( F "s R ) |
2 |
|
imasmndf1.v |
|- V = ( Base ` R ) |
3 |
1
|
a1i |
|- ( ( F : V -1-1-> B /\ R e. Mnd ) -> U = ( F "s R ) ) |
4 |
2
|
a1i |
|- ( ( F : V -1-1-> B /\ R e. Mnd ) -> V = ( Base ` R ) ) |
5 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
6 |
|
f1f1orn |
|- ( F : V -1-1-> B -> F : V -1-1-onto-> ran F ) |
7 |
6
|
adantr |
|- ( ( F : V -1-1-> B /\ R e. 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 e. Mnd ) -> F : V -onto-> ran F ) |
10 |
7
|
f1ocpbl |
|- ( ( ( F : V -1-1-> B /\ R e. Mnd ) /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) ) |
11 |
|
simpr |
|- ( ( F : V -1-1-> B /\ R e. Mnd ) -> R e. Mnd ) |
12 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
13 |
3 4 5 9 10 11 12
|
imasmnd |
|- ( ( F : V -1-1-> B /\ R e. Mnd ) -> ( U e. Mnd /\ ( F ` ( 0g ` R ) ) = ( 0g ` U ) ) ) |
14 |
13
|
simpld |
|- ( ( F : V -1-1-> B /\ R e. Mnd ) -> U e. Mnd ) |