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 
|- A e. SH
shlesb1.2 
|- B e. SH
Assertion shsval2i 
|- ( A +H B ) = |^| { x e. SH | ( A u. B ) C_ x }

Proof

Step Hyp Ref Expression
1 shlesb1.1 
 |-  A e. SH
2 shlesb1.2 
 |-  B e. SH
3 ssun1 
 |-  A C_ ( A u. B )
4 ssintub 
 |-  ( A u. B ) C_ |^| { x e. SH | ( A u. B ) C_ x }
5 3 4 sstri 
 |-  A C_ |^| { x e. SH | ( A u. B ) C_ x }
6 ssun2 
 |-  B C_ ( A u. B )
7 6 4 sstri 
 |-  B C_ |^| { x e. SH | ( A u. B ) C_ x }
8 5 7 pm3.2i 
 |-  ( A C_ |^| { x e. SH | ( A u. B ) C_ x } /\ B C_ |^| { x e. SH | ( A u. B ) C_ x } )
9 ssrab2 
 |-  { x e. SH | ( A u. B ) C_ x } C_ SH
10 1 2 shscli 
 |-  ( A +H B ) e. SH
11 1 2 shunssi 
 |-  ( A u. B ) C_ ( A +H B )
12 sseq2 
 |-  ( x = ( A +H B ) -> ( ( A u. B ) C_ x <-> ( A u. B ) C_ ( A +H B ) ) )
13 12 rspcev 
 |-  ( ( ( A +H B ) e. SH /\ ( A u. B ) C_ ( A +H B ) ) -> E. x e. SH ( A u. B ) C_ x )
14 10 11 13 mp2an 
 |-  E. x e. SH ( A u. B ) C_ x
15 rabn0 
 |-  ( { x e. SH | ( A u. B ) C_ x } =/= (/) <-> E. x e. SH ( A u. B ) C_ x )
16 14 15 mpbir 
 |-  { x e. SH | ( A u. B ) C_ x } =/= (/)
17 shintcl 
 |-  ( ( { x e. SH | ( A u. B ) C_ x } C_ SH /\ { x e. SH | ( A u. B ) C_ x } =/= (/) ) -> |^| { x e. SH | ( A u. B ) C_ x } e. SH )
18 9 16 17 mp2an 
 |-  |^| { x e. SH | ( A u. B ) C_ x } e. SH
19 1 2 18 shslubi 
 |-  ( ( A C_ |^| { x e. SH | ( A u. B ) C_ x } /\ B C_ |^| { x e. SH | ( A u. B ) C_ x } ) <-> ( A +H B ) C_ |^| { x e. SH | ( A u. B ) C_ x } )
20 8 19 mpbi 
 |-  ( A +H B ) C_ |^| { x e. SH | ( A u. B ) C_ x }
21 12 elrab 
 |-  ( ( A +H B ) e. { x e. SH | ( A u. B ) C_ x } <-> ( ( A +H B ) e. SH /\ ( A u. B ) C_ ( A +H B ) ) )
22 10 11 21 mpbir2an 
 |-  ( A +H B ) e. { x e. SH | ( A u. B ) C_ x }
23 intss1 
 |-  ( ( A +H B ) e. { x e. SH | ( A u. B ) C_ x } -> |^| { x e. SH | ( A u. B ) C_ x } C_ ( A +H B ) )
24 22 23 ax-mp 
 |-  |^| { x e. SH | ( A u. B ) C_ x } C_ ( A +H B )
25 20 24 eqssi 
 |-  ( A +H B ) = |^| { x e. SH | ( A u. B ) C_ x }