Metamath Proof Explorer

Theorem dochord2N

Description: Ordering law for orthocomplement. (Contributed by NM, 29-Oct-2014) (New usage is discouraged.)

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

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 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ⊢ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
9 1 7 2 8 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
10 4 5 9 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
11 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
12 11 8 lssss ⊢ ( 𝑋 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
13 10 12 syl ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 1 2 7 11 3 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 )
15 4 13 14 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ran 𝐼 )
16 1 2 3 4 15 6 dochord ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ⊆ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) )
17 1 2 3 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
18 4 5 17 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
19 18 sseq2d ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ↔ ( ⊥ ‘ 𝑌 ) ⊆ 𝑋 ) )
20 16 19 bitrd ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ⊆ 𝑌 ↔ ( ⊥ ‘ 𝑌 ) ⊆ 𝑋 ) )