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 }