Metamath Proof Explorer

Theorem cssincl

Description: The zero subspace is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis css0.c ⊢ C = ClSubSp ⁡ W
Assertion cssincl ⊢ W ∈ PreHil ∧ A ∈ C ∧ B ∈ C → A ∩ B ∈ C

Proof

Step Hyp Ref Expression
1 css0.c ⊢ C = ClSubSp ⁡ W
2 eqid ⊢ Base W = Base W
3 eqid ⊢ ocv ⁡ W = ocv ⁡ W
4 2 3 ocvss ⊢ ocv ⁡ W ⁡ A ⊆ Base W
5 2 3 ocvss ⊢ ocv ⁡ W ⁡ B ⊆ Base W
6 4 5 unssi ⊢ ocv ⁡ W ⁡ A ∪ ocv ⁡ W ⁡ B ⊆ Base W
7 2 1 3 ocvcss ⊢ W ∈ PreHil ∧ ocv ⁡ W ⁡ A ∪ ocv ⁡ W ⁡ B ⊆ Base W → ocv ⁡ W ⁡ ocv ⁡ W ⁡ A ∪ ocv ⁡ W ⁡ B ∈ C
8 6 7 mpan2 ⊢ W ∈ PreHil → ocv ⁡ W ⁡ ocv ⁡ W ⁡ A ∪ ocv ⁡ W ⁡ B ∈ C
9 3 1 cssi ⊢ A ∈ C → A = ocv ⁡ W ⁡ ocv ⁡ W ⁡ A
10 3 1 cssi ⊢ B ∈ C → B = ocv ⁡ W ⁡ ocv ⁡ W ⁡ B
11 9 10 ineqan12d ⊢ A ∈ C ∧ B ∈ C → A ∩ B = ocv ⁡ W ⁡ ocv ⁡ W ⁡ A ∩ ocv ⁡ W ⁡ ocv ⁡ W ⁡ B
12 3 unocv ⊢ ocv ⁡ W ⁡ ocv ⁡ W ⁡ A ∪ ocv ⁡ W ⁡ B = ocv ⁡ W ⁡ ocv ⁡ W ⁡ A ∩ ocv ⁡ W ⁡ ocv ⁡ W ⁡ B
13 11 12 eqtr4di ⊢ A ∈ C ∧ B ∈ C → A ∩ B = ocv ⁡ W ⁡ ocv ⁡ W ⁡ A ∪ ocv ⁡ W ⁡ B
14 13 eleq1d ⊢ A ∈ C ∧ B ∈ C → A ∩ B ∈ C ↔ ocv ⁡ W ⁡ ocv ⁡ W ⁡ A ∪ ocv ⁡ W ⁡ B ∈ C
15 8 14 syl5ibrcom ⊢ W ∈ PreHil → A ∈ C ∧ B ∈ C → A ∩ B ∈ C
16 15 3impib ⊢ W ∈ PreHil ∧ A ∈ C ∧ B ∈ C → A ∩ B ∈ C