Theorem spansnscl

Description: The subspace sum of a closed subspace and a one-dimensional subspace is closed. (Contributed by NM, 17-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	spansnscl	|- ( ( A e. CH /\ B e. ~H ) -> ( A +H ( span ` { B } ) ) e. CH )

Proof

Step	Hyp	Ref	Expression
1		spansnj	|- ( ( A e. CH /\ B e. ~H ) -> ( A +H ( span ` { B } ) ) = ( A vH ( span ` { B } ) ) )
2		spansnch	|- ( B e. ~H -> ( span ` { B } ) e. CH )
3		chjcl	|- ( ( A e. CH /\ ( span ` { B } ) e. CH ) -> ( A vH ( span ` { B } ) ) e. CH )
4	2 3	sylan2	|- ( ( A e. CH /\ B e. ~H ) -> ( A vH ( span ` { B } ) ) e. CH )
5	1 4	eqeltrd	|- ( ( A e. CH /\ B e. ~H ) -> ( A +H ( span ` { B } ) ) e. CH )