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 ∣ ( 𝐴𝐵 ) ⊆ 𝑥 }