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

Metamath Proof Explorer

Theorem shsval2i

Description: An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses shlesb1.1 ⊢ 𝐴 ∈ Sℋ
shlesb1.2 ⊢ 𝐵 ∈ Sℋ
Assertion shsval2i ( 𝐴 +ℋ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }

Proof

Step Hyp Ref Expression
1 shlesb1.1 ⊢ 𝐴 ∈ Sℋ
2 shlesb1.2 ⊢ 𝐵 ∈ Sℋ
3 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
4 ssintub ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
5 3 4 sstri ⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
6 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
7 6 4 sstri ⊢ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
8 5 7 pm3.2i ⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∧ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } )
9 ssrab2 ⊢ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ Sℋ
10 1 2 shscli ⊢ ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ
11 1 2 shunssi ⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 )
12 sseq2 ⊢ ( 𝑥 = ( 𝐴 +ℋ 𝐵 ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
13 12 rspcev ⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) → ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 )
14 10 11 13 mp2an ⊢ ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥
15 rabn0 ⊢ ( { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 )
16 14 15 mpbir ⊢ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅
17 shintcl ⊢ ( ( { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ Sℋ ∧ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅ ) → ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∈ Sℋ )
18 9 16 17 mp2an ⊢ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∈ Sℋ
19 1 2 18 shslubi ⊢ ( ( 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∧ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ) ↔ ( 𝐴 +ℋ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } )
20 8 19 mpbi ⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
21 12 elrab ⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ↔ ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
22 10 11 21 mpbir2an ⊢ ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }
23 intss1 ⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } → ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ ( 𝐴 +ℋ 𝐵 ) )
24 22 23 ax-mp ⊢ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ ( 𝐴 +ℋ 𝐵 )
25 20 24 eqssi ⊢ ( 𝐴 +ℋ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 }