Metamath Proof Explorer

Theorem dochord

Description: Ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014)

Ref Expression
Hypotheses doch11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
doch11.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
doch11.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
doch11.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
doch11.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
doch11.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
Assertion dochord ( 𝜑 → ( 𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 doch11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 doch11.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 doch11.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 doch11.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
5 doch11.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
6 doch11.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
7 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
10 1 8 2 9 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → 𝑌 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
11 4 6 10 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → 𝑌 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝑌 )
14 1 8 9 3 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )
15 7 12 13 14 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )
16 4 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 1 8 2 9 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
18 4 5 17 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
19 1 2 8 9 3 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 )
20 4 18 19 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 )
21 1 8 2 9 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 ) → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
22 4 20 21 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
24 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )
25 1 8 9 3 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
26 16 23 24 25 syl3anc ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
27 1 2 3 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
28 4 5 27 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
30 1 2 3 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
31 4 6 30 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
33 26 29 32 3sstr3d ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → 𝑋 ⊆ 𝑌 )
34 15 33 impbida ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) )