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

Metamath Proof Explorer

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ℋ )