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

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 ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion cssincl ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 )

Proof

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