Step |
Hyp |
Ref |
Expression |
1 |
|
symgov.1 |
|- G = ( SymGrp ` A ) |
2 |
|
symgov.2 |
|- B = ( Base ` G ) |
3 |
|
symgov.3 |
|- .+ = ( +g ` G ) |
4 |
1 2 3
|
symgov |
|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) ) |
5 |
1 2
|
symgbasf1o |
|- ( X e. B -> X : A -1-1-onto-> A ) |
6 |
1 2
|
symgbasf1o |
|- ( Y e. B -> Y : A -1-1-onto-> A ) |
7 |
|
f1oco |
|- ( ( X : A -1-1-onto-> A /\ Y : A -1-1-onto-> A ) -> ( X o. Y ) : A -1-1-onto-> A ) |
8 |
5 6 7
|
syl2an |
|- ( ( X e. B /\ Y e. B ) -> ( X o. Y ) : A -1-1-onto-> A ) |
9 |
|
coexg |
|- ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. _V ) |
10 |
1 2
|
elsymgbas2 |
|- ( ( X o. Y ) e. _V -> ( ( X o. Y ) e. B <-> ( X o. Y ) : A -1-1-onto-> A ) ) |
11 |
9 10
|
syl |
|- ( ( X e. B /\ Y e. B ) -> ( ( X o. Y ) e. B <-> ( X o. Y ) : A -1-1-onto-> A ) ) |
12 |
8 11
|
mpbird |
|- ( ( X e. B /\ Y e. B ) -> ( X o. Y ) e. B ) |
13 |
4 12
|
eqeltrd |
|- ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) e. B ) |