Metamath Proof Explorer

Definition df-pautN

Description: Define set of all projective automorphisms. This is the intended definition of automorphism in Crawley p. 112. (Contributed by NM, 26-Jan-2012)

Ref Expression
Assertion df-pautN 
|- PAut = ( k e. _V |-> { f | ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpautN 
 |-  PAut
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vf 
 |-  f
4 3 cv 
 |-  f
5 cpsubsp 
 |-  PSubSp
6 1 cv 
 |-  k
7 6 5 cfv 
 |-  ( PSubSp ` k )
8 7 7 4 wf1o 
 |-  f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k )
9 vx 
 |-  x
10 vy 
 |-  y
11 9 cv 
 |-  x
12 10 cv 
 |-  y
13 11 12 wss 
 |-  x C_ y
14 11 4 cfv 
 |-  ( f ` x )
15 12 4 cfv 
 |-  ( f ` y )
16 14 15 wss 
 |-  ( f ` x ) C_ ( f ` y )
17 13 16 wb 
 |-  ( x C_ y <-> ( f ` x ) C_ ( f ` y ) )
18 17 10 7 wral 
 |-  A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) )
19 18 9 7 wral 
 |-  A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) )
20 8 19 wa 
 |-  ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) )
21 20 3 cab 
 |-  { f | ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) }
22 1 2 21 cmpt 
 |-  ( k e. _V |-> { f | ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } )
23 0 22 wceq 
 |-  PAut = ( k e. _V |-> { f | ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } )