Theorem iscvlat2N

Description: The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	iscvlat2.b	|- B = ( Base ` K )
	iscvlat2.l	|- .<_ = ( le ` K )
	iscvlat2.j	|- .\/ = ( join ` K )
	iscvlat2.m	|- ./\ = ( meet ` K )
	iscvlat2.z	|- .0. = ( 0. ` K )
	iscvlat2.a	|- A = ( Atoms ` K )
Assertion	iscvlat2N	|- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscvlat2.b	|- B = ( Base ` K )
2		iscvlat2.l	|- .<_ = ( le ` K )
3		iscvlat2.j	|- .\/ = ( join ` K )
4		iscvlat2.m	|- ./\ = ( meet ` K )
5		iscvlat2.z	|- .0. = ( 0. ` K )
6		iscvlat2.a	|- A = ( Atoms ` K )
7	1 2 3 6	iscvlat	|- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
8		simpll	|- ( ( ( K e. AtLat /\ ( p e. A /\ q e. A ) ) /\ x e. B ) -> K e. AtLat )
9		simplrl	|- ( ( ( K e. AtLat /\ ( p e. A /\ q e. A ) ) /\ x e. B ) -> p e. A )
10		simpr	|- ( ( ( K e. AtLat /\ ( p e. A /\ q e. A ) ) /\ x e. B ) -> x e. B )
11	1 2 4 5 6	atnle	|- ( ( K e. AtLat /\ p e. A /\ x e. B ) -> ( -. p .<_ x <-> ( p ./\ x ) = .0. ) )
12	8 9 10 11	syl3anc	|- ( ( ( K e. AtLat /\ ( p e. A /\ q e. A ) ) /\ x e. B ) -> ( -. p .<_ x <-> ( p ./\ x ) = .0. ) )
13	12	anbi1d	|- ( ( ( K e. AtLat /\ ( p e. A /\ q e. A ) ) /\ x e. B ) -> ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) <-> ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) ) )
14	13	imbi1d	|- ( ( ( K e. AtLat /\ ( p e. A /\ q e. A ) ) /\ x e. B ) -> ( ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) <-> ( ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
15	14	ralbidva	|- ( ( K e. AtLat /\ ( p e. A /\ q e. A ) ) -> ( A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) <-> A. x e. B ( ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
16	15	2ralbidva	|- ( K e. AtLat -> ( A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) <-> A. p e. A A. q e. A A. x e. B ( ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
17	16	pm5.32i	|- ( ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
18	7 17	bitri	|- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )