Theorem 1cvrco

Description: The orthocomplement of an element covered by 1 is an atom. (Contributed by NM, 7-May-2012)

	Ref	Expression
Hypotheses	1cvrco.b	|- B = ( Base ` K )
	1cvrco.u	|- .1. = ( 1. ` K )
	1cvrco.o	|- ._|_ = ( oc ` K )
	1cvrco.c	|- C = (
	1cvrco.a	|- A = ( Atoms ` K )
Assertion	1cvrco	|- ( ( K e. HL /\ X e. B ) -> ( X C .1. <-> ( ._|_ ` X ) e. A ) )

Proof

Step	Hyp	Ref	Expression
1		1cvrco.b	|- B = ( Base ` K )
2		1cvrco.u	|- .1. = ( 1. ` K )
3		1cvrco.o	|- ._|_ = ( oc ` K )
4		1cvrco.c	|- C = (
5		1cvrco.a	|- A = ( Atoms ` K )
6		hlop	|- ( K e. HL -> K e. OP )
7	6	adantr	|- ( ( K e. HL /\ X e. B ) -> K e. OP )
8		simpr	|- ( ( K e. HL /\ X e. B ) -> X e. B )
9	1 2	op1cl	|- ( K e. OP -> .1. e. B )
10	7 9	syl	|- ( ( K e. HL /\ X e. B ) -> .1. e. B )
11	1 3 4	cvrcon3b	|- ( ( K e. OP /\ X e. B /\ .1. e. B ) -> ( X C .1. <-> ( ._|_ ` .1. ) C ( ._|_ ` X ) ) )
12	7 8 10 11	syl3anc	|- ( ( K e. HL /\ X e. B ) -> ( X C .1. <-> ( ._|_ ` .1. ) C ( ._|_ ` X ) ) )
13		eqid	|- ( 0. ` K ) = ( 0. ` K )
14	13 2 3	opoc1	|- ( K e. OP -> ( ._|_ ` .1. ) = ( 0. ` K ) )
15	7 14	syl	|- ( ( K e. HL /\ X e. B ) -> ( ._|_ ` .1. ) = ( 0. ` K ) )
16	15	breq1d	|- ( ( K e. HL /\ X e. B ) -> ( ( ._|_ ` .1. ) C ( ._|_ ` X ) <-> ( 0. ` K ) C ( ._|_ ` X ) ) )
17	1 3	opoccl	|- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
18	6 17	sylan	|- ( ( K e. HL /\ X e. B ) -> ( ._|_ ` X ) e. B )
19	18	biantrurd	|- ( ( K e. HL /\ X e. B ) -> ( ( 0. ` K ) C ( ._|_ ` X ) <-> ( ( ._|_ ` X ) e. B /\ ( 0. ` K ) C ( ._|_ ` X ) ) ) )
20	12 16 19	3bitrd	|- ( ( K e. HL /\ X e. B ) -> ( X C .1. <-> ( ( ._|_ ` X ) e. B /\ ( 0. ` K ) C ( ._|_ ` X ) ) ) )
21	1 13 4 5	isat	|- ( K e. HL -> ( ( ._|_ ` X ) e. A <-> ( ( ._|_ ` X ) e. B /\ ( 0. ` K ) C ( ._|_ ` X ) ) ) )
22	21	adantr	|- ( ( K e. HL /\ X e. B ) -> ( ( ._|_ ` X ) e. A <-> ( ( ._|_ ` X ) e. B /\ ( 0. ` K ) C ( ._|_ ` X ) ) ) )
23	20 22	bitr4d	|- ( ( K e. HL /\ X e. B ) -> ( X C .1. <-> ( ._|_ ` X ) e. A ) )