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

Metamath Proof Explorer

Theorem shintcl

Description: The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shintcl ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Sℋ )

Proof

Step Hyp Ref Expression
1 inteq ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ∩ 𝐴 = ∩ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) )
2 1 eleq1d ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( ∩ 𝐴 ∈ Sℋ ↔ ∩ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ∈ Sℋ ) )
3 sseq1 ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( 𝐴 ⊆ Sℋ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ) )
4 neeq1 ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( 𝐴 ≠ ∅ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) )
5 3 4 anbi12d ⊢ ( 𝐴 = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) ↔ ( if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ∧ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) ) )
6 sseq1 ⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( Sℋ ⊆ Sℋ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ) )
7 neeq1 ⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( Sℋ ≠ ∅ ↔ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) )
8 6 7 anbi12d ⊢ ( Sℋ = if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) → ( ( Sℋ ⊆ Sℋ ∧ Sℋ ≠ ∅ ) ↔ ( if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ∧ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ ) ) )
9 ssid ⊢ Sℋ ⊆ Sℋ
10 h0elsh ⊢ 0ℋ ∈ Sℋ
11 10 ne0ii ⊢ Sℋ ≠ ∅
12 9 11 pm3.2i ⊢ ( Sℋ ⊆ Sℋ ∧ Sℋ ≠ ∅ )
13 5 8 12 elimhyp ⊢ ( if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ⊆ Sℋ ∧ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ≠ ∅ )
14 13 shintcli ⊢ ∩ if ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) , 𝐴 , Sℋ ) ∈ Sℋ
15 2 14 dedth ⊢ ( ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ Sℋ )