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