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 ⊢ H = LHyp ⁡ K
dochsscl.u ⊢ U = DVecH ⁡ K ⁡ W
dochsscl.v ⊢ V = Base U
dochsscl.i ⊢ I = DIsoH ⁡ K ⁡ W
dochsscl.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochsscl.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochsscl.x ⊢ φ → X ⊆ V
dochsscl.y ⊢ φ → Y ∈ ran ⁡ I
Assertion dochsscl ⊢ φ → X ⊆ Y ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ Y

Proof

Step Hyp Ref Expression
1 dochsscl.h ⊢ H = LHyp ⁡ K
2 dochsscl.u ⊢ U = DVecH ⁡ K ⁡ W
3 dochsscl.v ⊢ V = Base U
4 dochsscl.i ⊢ I = DIsoH ⁡ K ⁡ W
5 dochsscl.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
6 dochsscl.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dochsscl.x ⊢ φ → X ⊆ V
8 dochsscl.y ⊢ φ → Y ∈ ran ⁡ I
9 6 adantr ⊢ φ ∧ X ⊆ Y → K ∈ HL ∧ W ∈ H
10 7 adantr ⊢ φ ∧ X ⊆ Y → X ⊆ V
11 1 2 3 5 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ⊆ V
12 9 10 11 syl2anc ⊢ φ ∧ X ⊆ Y → ⊥ ˙ ⁡ X ⊆ V
13 1 2 4 3 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → Y ⊆ V
14 6 8 13 syl2anc ⊢ φ → Y ⊆ V
15 14 adantr ⊢ φ ∧ X ⊆ Y → Y ⊆ V
16 simpr ⊢ φ ∧ X ⊆ Y → X ⊆ Y
17 1 2 3 5 dochss ⊢ K ∈ HL ∧ W ∈ H ∧ Y ⊆ V ∧ X ⊆ Y → ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X
18 9 15 16 17 syl3anc ⊢ φ ∧ X ⊆ Y → ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X
19 1 2 3 5 dochss ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ⊆ V ∧ ⊥ ˙ ⁡ Y ⊆ ⊥ ˙ ⁡ X → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
20 9 12 18 19 syl3anc ⊢ φ ∧ X ⊆ Y → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
21 8 adantr ⊢ φ ∧ X ⊆ Y → Y ∈ ran ⁡ I
22 1 4 5 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
23 9 21 22 syl2anc ⊢ φ ∧ X ⊆ Y → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
24 20 23 sseqtrd ⊢ φ ∧ X ⊆ Y → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ Y
25 1 2 3 5 dochocss ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
26 6 7 25 syl2anc ⊢ φ → X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X
27 sstr ⊢ X ⊆ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ Y → X ⊆ Y
28 26 27 sylan ⊢ φ ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ Y → X ⊆ Y
29 24 28 impbida ⊢ φ → X ⊆ Y ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ⊆ Y