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 ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐶 )