Theorem islpln2

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012)

	Ref	Expression
Hypotheses	islpln5.b	|- B = ( Base ` K )
	islpln5.l	|- .<_ = ( le ` K )
	islpln5.j	|- .\/ = ( join ` K )
	islpln5.a	|- A = ( Atoms ` K )
	islpln5.p	|- P = ( LPlanes ` K )
Assertion	islpln2	|- ( K e. HL -> ( X e. P <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islpln5.b	|- B = ( Base ` K )
2		islpln5.l	|- .<_ = ( le ` K )
3		islpln5.j	|- .\/ = ( join ` K )
4		islpln5.a	|- A = ( Atoms ` K )
5		islpln5.p	|- P = ( LPlanes ` K )
6	1 5	lplnbase	|- ( X e. P -> X e. B )
7	6	pm4.71ri	|- ( X e. P <-> ( X e. B /\ X e. P ) )
8	1 2 3 4 5	islpln5	|- ( ( K e. HL /\ X e. B ) -> ( X e. P <-> E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
9	8	pm5.32da	|- ( K e. HL -> ( ( X e. B /\ X e. P ) <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )
10	7 9	bitrid	|- ( K e. HL -> ( X e. P <-> ( X e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )