Theorem shincl

Description: Closure of intersection of two subspaces. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	shincl	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Sℋ )

Proof

Step	Hyp	Ref	Expression
1		ineq1	⊢ ( 𝐴 = if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) → ( 𝐴 ∩ 𝐵 ) = ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∩ 𝐵 ) )
2	1	eleq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) → ( ( 𝐴 ∩ 𝐵 ) ∈ Sℋ ↔ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∩ 𝐵 ) ∈ Sℋ ) )
3		ineq2	⊢ ( 𝐵 = if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) → ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∩ 𝐵 ) = ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∩ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) )
4	3	eleq1d	⊢ ( 𝐵 = if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) → ( ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∩ 𝐵 ) ∈ Sℋ ↔ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∩ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) ∈ Sℋ ) )
5		helsh	⊢ ℋ ∈ Sℋ
6	5	elimel	⊢ if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∈ Sℋ
7	5	elimel	⊢ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ∈ Sℋ
8	6 7	shincli	⊢ ( if ( 𝐴 ∈ Sℋ , 𝐴 , ℋ ) ∩ if ( 𝐵 ∈ Sℋ , 𝐵 , ℋ ) ) ∈ Sℋ
9	2 4 8	dedth2h	⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Sℋ )