Metamath Proof Explorer

Theorem ispsubsp2

Description: The predicate "is 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	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 ) ) ) )

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	ispsubsp	\|- ( K e. D -> ( X e. S <-> ( X C_ A /\ A. q e. X A. r e. X A. p e. A ( p .<_ ( q .\/ r ) -> p e. X ) ) ) )
6		ralcom	\|- ( A. r e. X A. p e. A ( p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A A. r e. X ( p .<_ ( q .\/ r ) -> p e. X ) )
7		r19.23v	\|- ( A. r e. X ( p .<_ ( q .\/ r ) -> p e. X ) <-> ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
8	7	ralbii	\|- ( A. p e. A A. r e. X ( p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
9	6 8	bitri	\|- ( A. r e. X A. p e. A ( p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
10	9	ralbii	\|- ( A. q e. X A. r e. X A. p e. A ( p .<_ ( q .\/ r ) -> p e. X ) <-> A. q e. X A. p e. A ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
11		ralcom	\|- ( A. q e. X A. p e. A ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A A. q e. X ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
12		r19.23v	\|- ( A. 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 ) )
13	12	ralbii	\|- ( A. p e. A A. q e. X ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
14	11 13	bitri	\|- ( A. q e. X A. p e. A ( E. r e. X p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
15	10 14	bitri	\|- ( A. q e. X A. r e. X A. p e. A ( p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) )
16	15	a1i	\|- ( K e. D -> ( A. q e. X A. r e. X A. p e. A ( p .<_ ( q .\/ r ) -> p e. X ) <-> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) ) )
17	16	anbi2d	\|- ( K e. D -> ( ( X C_ A /\ A. q e. X A. r e. X A. p e. A ( p .<_ ( q .\/ r ) -> p e. X ) ) <-> ( X C_ A /\ A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) ) ) )
18	5 17	bitrd	\|- ( 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 ) ) ) )