Step |
Hyp |
Ref |
Expression |
1 |
|
grposnOLD.1 |
|- A e. _V |
2 |
|
snex |
|- { A } e. _V |
3 |
|
opex |
|- <. A , A >. e. _V |
4 |
3 1
|
f1osn |
|- { <. <. A , A >. , A >. } : { <. A , A >. } -1-1-onto-> { A } |
5 |
|
f1of |
|- ( { <. <. A , A >. , A >. } : { <. A , A >. } -1-1-onto-> { A } -> { <. <. A , A >. , A >. } : { <. A , A >. } --> { A } ) |
6 |
4 5
|
ax-mp |
|- { <. <. A , A >. , A >. } : { <. A , A >. } --> { A } |
7 |
1 1
|
xpsn |
|- ( { A } X. { A } ) = { <. A , A >. } |
8 |
7
|
feq2i |
|- ( { <. <. A , A >. , A >. } : ( { A } X. { A } ) --> { A } <-> { <. <. A , A >. , A >. } : { <. A , A >. } --> { A } ) |
9 |
6 8
|
mpbir |
|- { <. <. A , A >. , A >. } : ( { A } X. { A } ) --> { A } |
10 |
|
velsn |
|- ( x e. { A } <-> x = A ) |
11 |
|
velsn |
|- ( y e. { A } <-> y = A ) |
12 |
|
velsn |
|- ( z e. { A } <-> z = A ) |
13 |
|
oveq2 |
|- ( z = A -> ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } z ) = ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } A ) ) |
14 |
|
oveq1 |
|- ( x = A -> ( x { <. <. A , A >. , A >. } y ) = ( A { <. <. A , A >. , A >. } y ) ) |
15 |
|
oveq2 |
|- ( y = A -> ( A { <. <. A , A >. , A >. } y ) = ( A { <. <. A , A >. , A >. } A ) ) |
16 |
|
df-ov |
|- ( A { <. <. A , A >. , A >. } A ) = ( { <. <. A , A >. , A >. } ` <. A , A >. ) |
17 |
3 1
|
fvsn |
|- ( { <. <. A , A >. , A >. } ` <. A , A >. ) = A |
18 |
16 17
|
eqtri |
|- ( A { <. <. A , A >. , A >. } A ) = A |
19 |
15 18
|
eqtrdi |
|- ( y = A -> ( A { <. <. A , A >. , A >. } y ) = A ) |
20 |
14 19
|
sylan9eq |
|- ( ( x = A /\ y = A ) -> ( x { <. <. A , A >. , A >. } y ) = A ) |
21 |
20
|
oveq1d |
|- ( ( x = A /\ y = A ) -> ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } A ) = ( A { <. <. A , A >. , A >. } A ) ) |
22 |
21 18
|
eqtrdi |
|- ( ( x = A /\ y = A ) -> ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } A ) = A ) |
23 |
13 22
|
sylan9eqr |
|- ( ( ( x = A /\ y = A ) /\ z = A ) -> ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } z ) = A ) |
24 |
23
|
3impa |
|- ( ( x = A /\ y = A /\ z = A ) -> ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } z ) = A ) |
25 |
|
oveq1 |
|- ( x = A -> ( x { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) = ( A { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) ) |
26 |
|
oveq1 |
|- ( y = A -> ( y { <. <. A , A >. , A >. } z ) = ( A { <. <. A , A >. , A >. } z ) ) |
27 |
|
oveq2 |
|- ( z = A -> ( A { <. <. A , A >. , A >. } z ) = ( A { <. <. A , A >. , A >. } A ) ) |
28 |
27 18
|
eqtrdi |
|- ( z = A -> ( A { <. <. A , A >. , A >. } z ) = A ) |
29 |
26 28
|
sylan9eq |
|- ( ( y = A /\ z = A ) -> ( y { <. <. A , A >. , A >. } z ) = A ) |
30 |
29
|
oveq2d |
|- ( ( y = A /\ z = A ) -> ( A { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) = ( A { <. <. A , A >. , A >. } A ) ) |
31 |
30 18
|
eqtrdi |
|- ( ( y = A /\ z = A ) -> ( A { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) = A ) |
32 |
25 31
|
sylan9eq |
|- ( ( x = A /\ ( y = A /\ z = A ) ) -> ( x { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) = A ) |
33 |
32
|
3impb |
|- ( ( x = A /\ y = A /\ z = A ) -> ( x { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) = A ) |
34 |
24 33
|
eqtr4d |
|- ( ( x = A /\ y = A /\ z = A ) -> ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } z ) = ( x { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) ) |
35 |
10 11 12 34
|
syl3anb |
|- ( ( x e. { A } /\ y e. { A } /\ z e. { A } ) -> ( ( x { <. <. A , A >. , A >. } y ) { <. <. A , A >. , A >. } z ) = ( x { <. <. A , A >. , A >. } ( y { <. <. A , A >. , A >. } z ) ) ) |
36 |
1
|
snid |
|- A e. { A } |
37 |
|
oveq2 |
|- ( x = A -> ( A { <. <. A , A >. , A >. } x ) = ( A { <. <. A , A >. , A >. } A ) ) |
38 |
37 18
|
eqtrdi |
|- ( x = A -> ( A { <. <. A , A >. , A >. } x ) = A ) |
39 |
|
id |
|- ( x = A -> x = A ) |
40 |
38 39
|
eqtr4d |
|- ( x = A -> ( A { <. <. A , A >. , A >. } x ) = x ) |
41 |
10 40
|
sylbi |
|- ( x e. { A } -> ( A { <. <. A , A >. , A >. } x ) = x ) |
42 |
36
|
a1i |
|- ( x e. { A } -> A e. { A } ) |
43 |
10 38
|
sylbi |
|- ( x e. { A } -> ( A { <. <. A , A >. , A >. } x ) = A ) |
44 |
2 9 35 36 41 42 43
|
isgrpoi |
|- { <. <. A , A >. , A >. } e. GrpOp |