This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( 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 ↔ ( ⊥ ‘ 𝑋 ) ∈ 𝐴 ) )