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

Metamath Proof Explorer

Theorem dochsscl

Description: If a set of vectors is included in a closed set, so is its closure. (Contributed by NM, 17-Jun-2015)

Ref Expression
Hypotheses dochsscl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochsscl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochsscl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochsscl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochsscl.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochsscl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochsscl.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
dochsscl.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
Assertion dochsscl ( 𝜑 → ( 𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 dochsscl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochsscl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dochsscl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dochsscl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 dochsscl.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6 dochsscl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochsscl.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
8 dochsscl.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
9 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝑉 )
11 1 2 3 5 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
12 9 10 11 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
13 1 2 4 3 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → 𝑌 ⊆ 𝑉 )
14 6 8 13 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → 𝑌 ⊆ 𝑉 )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → 𝑋 ⊆ 𝑌 )
17 1 2 3 5 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )
18 9 15 16 17 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )
19 1 2 3 5 dochss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
20 9 12 18 19 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
21 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → 𝑌 ∈ ran 𝐼 )
22 1 4 5 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
23 9 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
24 20 23 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑌 )
25 1 2 3 5 dochocss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
26 6 7 25 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
27 sstr ⊢ ( ( 𝑋 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑌 ) → 𝑋 ⊆ 𝑌 )
28 26 27 sylan ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑌 ) → 𝑋 ⊆ 𝑌 )
29 24 28 impbida ⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑌 ) )