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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	1cvrco.u	⊢ 1 = ( 1. ‘ 𝐾 )
	1cvrco.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	1cvrco.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	1cvrco.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	1cvrco	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 𝐶 1 ↔ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		1cvrco.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		1cvrco.u	⊢ 1 = ( 1. ‘ 𝐾 )
3		1cvrco.o	⊢ ⊥ = ( oc ‘ 𝐾 )
4		1cvrco.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5		1cvrco.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
7	6	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP )
8		simpr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
9	1 2	op1cl	⊢ ( 𝐾 ∈ OP → 1 ∈ 𝐵 )
10	7 9	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → 1 ∈ 𝐵 )
11	1 3 4	cvrcon3b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) → ( 𝑋 𝐶 1 ↔ ( ⊥ ‘ 1 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) )
12	7 8 10 11	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 𝐶 1 ↔ ( ⊥ ‘ 1 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) )
13		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
14	13 2 3	opoc1	⊢ ( 𝐾 ∈ OP → ( ⊥ ‘ 1 ) = ( 0. ‘ 𝐾 ) )
15	7 14	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 1 ) = ( 0. ‘ 𝐾 ) )
16	15	breq1d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( ⊥ ‘ 1 ) 𝐶 ( ⊥ ‘ 𝑋 ) ↔ ( 0. ‘ 𝐾 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) )
17	1 3	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
18	6 17	sylan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 )
19	18	biantrurd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( 0. ‘ 𝐾 ) 𝐶 ( ⊥ ‘ 𝑋 ) ↔ ( ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ ( 0. ‘ 𝐾 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) ) )
20	12 16 19	3bitrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 𝐶 1 ↔ ( ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ ( 0. ‘ 𝐾 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) ) )
21	1 13 4 5	isat	⊢ ( 𝐾 ∈ HL → ( ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ↔ ( ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ ( 0. ‘ 𝐾 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) ) )
22	21	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ↔ ( ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ ( 0. ‘ 𝐾 ) 𝐶 ( ⊥ ‘ 𝑋 ) ) ) )
23	20 22	bitr4d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 𝐶 1 ↔ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) )