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 }