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