Metamath Proof Explorer


Theorem grposnOLD

Description: The group operation for the singleton group. Obsolete, use grp1 . instead. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis grposnOLD.1
|- A e. _V
Assertion grposnOLD
|- { <. <. A , A >. , A >. } e. GrpOp

Proof

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