Step |
Hyp |
Ref |
Expression |
1 |
|
mgmb1mgm1.b |
|- B = ( Base ` M ) |
2 |
|
mgmb1mgm1.p |
|- .+ = ( +g ` M ) |
3 |
|
eqid |
|- ( +f ` M ) = ( +f ` M ) |
4 |
1 2 3
|
plusfeq |
|- ( .+ Fn ( B X. B ) -> ( +f ` M ) = .+ ) |
5 |
1 3
|
mgmplusf |
|- ( M e. Mgm -> ( +f ` M ) : ( B X. B ) --> B ) |
6 |
|
feq1 |
|- ( ( +f ` M ) = .+ -> ( ( +f ` M ) : ( B X. B ) --> B <-> .+ : ( B X. B ) --> B ) ) |
7 |
5 6
|
syl5ib |
|- ( ( +f ` M ) = .+ -> ( M e. Mgm -> .+ : ( B X. B ) --> B ) ) |
8 |
4 7
|
syl |
|- ( .+ Fn ( B X. B ) -> ( M e. Mgm -> .+ : ( B X. B ) --> B ) ) |
9 |
8
|
impcom |
|- ( ( M e. Mgm /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) --> B ) |
10 |
9
|
3adant2 |
|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) --> B ) |
11 |
|
simp2 |
|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> Z e. B ) |
12 |
|
intopsn |
|- ( ( .+ : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) ) |
13 |
10 11 12
|
syl2anc |
|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) ) |