Metamath Proof Explorer

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 = ⋖ K
1cvrco.a ⊢ A = Atoms ⁡ K
Assertion 1cvrco ⊢ K ∈ HL ∧ X ∈ B → X C 1 ˙ ↔ ⊥ ˙ ⁡ X ∈ 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 = ⋖ K
5 1cvrco.a ⊢ A = Atoms ⁡ K
6 hlop ⊢ K ∈ HL → K ∈ OP
7 6 adantr ⊢ K ∈ HL ∧ X ∈ B → K ∈ OP
8 simpr ⊢ K ∈ HL ∧ X ∈ B → X ∈ B
9 1 2 op1cl ⊢ K ∈ OP → 1 ˙ ∈ B
10 7 9 syl ⊢ K ∈ HL ∧ X ∈ B → 1 ˙ ∈ B
11 1 3 4 cvrcon3b ⊢ K ∈ OP ∧ X ∈ B ∧ 1 ˙ ∈ B → X C 1 ˙ ↔ ⊥ ˙ ⁡ 1 ˙ C ⊥ ˙ ⁡ X
12 7 8 10 11 syl3anc ⊢ K ∈ HL ∧ X ∈ B → X C 1 ˙ ↔ ⊥ ˙ ⁡ 1 ˙ C ⊥ ˙ ⁡ X
13 eqid ⊢ 0. ⁡ K = 0. ⁡ K
14 13 2 3 opoc1 ⊢ K ∈ OP → ⊥ ˙ ⁡ 1 ˙ = 0. ⁡ K
15 7 14 syl ⊢ K ∈ HL ∧ X ∈ B → ⊥ ˙ ⁡ 1 ˙ = 0. ⁡ K
16 15 breq1d ⊢ K ∈ HL ∧ X ∈ B → ⊥ ˙ ⁡ 1 ˙ C ⊥ ˙ ⁡ X ↔ 0. ⁡ K C ⊥ ˙ ⁡ X
17 1 3 opoccl ⊢ K ∈ OP ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B
18 6 17 sylan ⊢ K ∈ HL ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ B
19 18 biantrurd ⊢ K ∈ HL ∧ X ∈ B → 0. ⁡ K C ⊥ ˙ ⁡ X ↔ ⊥ ˙ ⁡ X ∈ B ∧ 0. ⁡ K C ⊥ ˙ ⁡ X
20 12 16 19 3bitrd ⊢ K ∈ HL ∧ X ∈ B → X C 1 ˙ ↔ ⊥ ˙ ⁡ X ∈ B ∧ 0. ⁡ K C ⊥ ˙ ⁡ X
21 1 13 4 5 isat ⊢ K ∈ HL → ⊥ ˙ ⁡ X ∈ A ↔ ⊥ ˙ ⁡ X ∈ B ∧ 0. ⁡ K C ⊥ ˙ ⁡ X
22 21 adantr ⊢ K ∈ HL ∧ X ∈ B → ⊥ ˙ ⁡ X ∈ A ↔ ⊥ ˙ ⁡ X ∈ B ∧ 0. ⁡ K C ⊥ ˙ ⁡ X
23 20 22 bitr4d ⊢ K ∈ HL ∧ X ∈ B → X C 1 ˙ ↔ ⊥ ˙ ⁡ X ∈ A