Theorem psubspi

Description: Property of a projective subspace. (Contributed by NM, 13-Jan-2012)

	Ref	Expression
Hypotheses	psubspset.l	|- .<_ = ( le ` K )
	psubspset.j	|- .\/ = ( join ` K )
	psubspset.a	|- A = ( Atoms ` K )
	psubspset.s	|- S = ( PSubSp ` K )
Assertion	psubspi	|- ( ( ( K e. D /\ X e. S /\ P e. A ) /\ E. q e. X E. r e. X P .<_ ( q .\/ r ) ) -> P 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	ispsubsp2	|- ( K e. D -> ( X e. S <-> ( X C_ A /\ A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) ) ) )
6	5	simplbda	|- ( ( K e. D /\ X e. S ) -> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
7	6	ex	|- ( K e. D -> ( X e. S -> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) ) )
8		breq1	|- ( p = P -> ( p .<_ ( q .\/ r ) <-> P .<_ ( q .\/ r ) ) )
9	8	2rexbidv	|- ( p = P -> ( E. q e. X E. r e. X p .<_ ( q .\/ r ) <-> E. q e. X E. r e. X P .<_ ( q .\/ r ) ) )
10		eleq1	|- ( p = P -> ( p e. X <-> P e. X ) )
11	9 10	imbi12d	|- ( p = P -> ( ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) <-> ( E. q e. X E. r e. X P .<_ ( q .\/ r ) -> P e. X ) ) )
12	11	rspccv	|- ( A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) -> ( P e. A -> ( E. q e. X E. r e. X P .<_ ( q .\/ r ) -> P e. X ) ) )
13	7 12	syl6	|- ( K e. D -> ( X e. S -> ( P e. A -> ( E. q e. X E. r e. X P .<_ ( q .\/ r ) -> P e. X ) ) ) )
14	13	3imp1	|- ( ( ( K e. D /\ X e. S /\ P e. A ) /\ E. q e. X E. r e. X P .<_ ( q .\/ r ) ) -> P e. X )