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=BaseK
1cvrco.u 1˙=1.K
1cvrco.o ˙=ocK
1cvrco.c C=K
1cvrco.a A=AtomsK
Assertion 1cvrco KHLXBXC1˙˙XA

Proof

Step Hyp Ref Expression
1 1cvrco.b B=BaseK
2 1cvrco.u 1˙=1.K
3 1cvrco.o ˙=ocK
4 1cvrco.c C=K
5 1cvrco.a A=AtomsK
6 hlop KHLKOP
7 6 adantr KHLXBKOP
8 simpr KHLXBXB
9 1 2 op1cl KOP1˙B
10 7 9 syl KHLXB1˙B
11 1 3 4 cvrcon3b KOPXB1˙BXC1˙˙1˙C˙X
12 7 8 10 11 syl3anc KHLXBXC1˙˙1˙C˙X
13 eqid 0.K=0.K
14 13 2 3 opoc1 KOP˙1˙=0.K
15 7 14 syl KHLXB˙1˙=0.K
16 15 breq1d KHLXB˙1˙C˙X0.KC˙X
17 1 3 opoccl KOPXB˙XB
18 6 17 sylan KHLXB˙XB
19 18 biantrurd KHLXB0.KC˙X˙XB0.KC˙X
20 12 16 19 3bitrd KHLXBXC1˙˙XB0.KC˙X
21 1 13 4 5 isat KHL˙XA˙XB0.KC˙X
22 21 adantr KHLXB˙XA˙XB0.KC˙X
23 20 22 bitr4d KHLXBXC1˙˙XA