Metamath Proof Explorer


Theorem ispautN

Description: The predictate "is a projective automorphism." (Contributed by NM, 26-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pautset.s
|- S = ( PSubSp ` K )
pautset.m
|- M = ( PAut ` K )
Assertion ispautN
|- ( K e. B -> ( F e. M <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pautset.s
 |-  S = ( PSubSp ` K )
2 pautset.m
 |-  M = ( PAut ` K )
3 1 2 pautsetN
 |-  ( K e. B -> M = { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } )
4 3 eleq2d
 |-  ( K e. B -> ( F e. M <-> F e. { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) )
5 f1of
 |-  ( F : S -1-1-onto-> S -> F : S --> S )
6 1 fvexi
 |-  S e. _V
7 fex
 |-  ( ( F : S --> S /\ S e. _V ) -> F e. _V )
8 5 6 7 sylancl
 |-  ( F : S -1-1-onto-> S -> F e. _V )
9 8 adantr
 |-  ( ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) -> F e. _V )
10 f1oeq1
 |-  ( f = F -> ( f : S -1-1-onto-> S <-> F : S -1-1-onto-> S ) )
11 fveq1
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
12 fveq1
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
13 11 12 sseq12d
 |-  ( f = F -> ( ( f ` x ) C_ ( f ` y ) <-> ( F ` x ) C_ ( F ` y ) ) )
14 13 bibi2d
 |-  ( f = F -> ( ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) )
15 14 2ralbidv
 |-  ( f = F -> ( A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) )
16 10 15 anbi12d
 |-  ( f = F -> ( ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) )
17 9 16 elab3
 |-  ( F e. { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) )
18 4 17 bitrdi
 |-  ( K e. B -> ( F e. M <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) )