Metamath Proof Explorer


Theorem ispsubsp

Description: The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011)

Ref Expression
Hypotheses psubspset.l
|- .<_ = ( le ` K )
psubspset.j
|- .\/ = ( join ` K )
psubspset.a
|- A = ( Atoms ` K )
psubspset.s
|- S = ( PSubSp ` K )
Assertion ispsubsp
|- ( K e. D -> ( X e. S <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) )

Proof

Step Hyp Ref Expression
1 psubspset.l
 |-  .<_ = ( le ` K )
2 psubspset.j
 |-  .\/ = ( join ` K )
3 psubspset.a
 |-  A = ( Atoms ` K )
4 psubspset.s
 |-  S = ( PSubSp ` K )
5 1 2 3 4 psubspset
 |-  ( K e. D -> S = { x | ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } )
6 5 eleq2d
 |-  ( K e. D -> ( X e. S <-> X e. { x | ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } ) )
7 3 fvexi
 |-  A e. _V
8 7 ssex
 |-  ( X C_ A -> X e. _V )
9 8 adantr
 |-  ( ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) -> X e. _V )
10 sseq1
 |-  ( x = X -> ( x C_ A <-> X C_ A ) )
11 eleq2
 |-  ( x = X -> ( r e. x <-> r e. X ) )
12 11 imbi2d
 |-  ( x = X -> ( ( r .<_ ( p .\/ q ) -> r e. x ) <-> ( r .<_ ( p .\/ q ) -> r e. X ) ) )
13 12 ralbidv
 |-  ( x = X -> ( A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
14 13 raleqbi1dv
 |-  ( x = X -> ( A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
15 14 raleqbi1dv
 |-  ( x = X -> ( A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
16 10 15 anbi12d
 |-  ( x = X -> ( ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) )
17 9 16 elab3
 |-  ( X e. { x | ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) )
18 6 17 bitrdi
 |-  ( K e. D -> ( X e. S <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) )