Theorem shsval3i

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	shsval3i	|- ( A +H B ) = ( span ` ( A u. B ) )

Proof

Step	Hyp	Ref	Expression
1		shlesb1.1	|- A e. SH
2		shlesb1.2	|- B e. SH
3	1 2	shsval2i	|- ( A +H B ) = |^| { x e. SH | ( A u. B ) C_ x }
4	1	shssii	|- A C_ ~H
5	2	shssii	|- B C_ ~H
6	4 5	unssi	|- ( A u. B ) C_ ~H
7		spanval	|- ( ( A u. B ) C_ ~H -> ( span ` ( A u. B ) ) = |^| { x e. SH | ( A u. B ) C_ x } )
8	6 7	ax-mp	|- ( span ` ( A u. B ) ) = |^| { x e. SH | ( A u. B ) C_ x }
9	3 8	eqtr4i	|- ( A +H B ) = ( span ` ( A u. B ) )