Theorem chjatom

Description: The join of a closed subspace and an atom equals their subspace sum. Special case of remark in Kalmbach p. 65, stating that if A or B is finite-dimensional, then this equality holds. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chjatom	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A +H B ) = ( A vH B ) )

Proof

Step	Hyp	Ref	Expression
1		atom1d	|- ( B e. HAtoms <-> E. x e. ~H ( x =/= 0h /\ B = ( span ` { x } ) ) )
2		spansnj	|- ( ( A e. CH /\ x e. ~H ) -> ( A +H ( span ` { x } ) ) = ( A vH ( span ` { x } ) ) )
3		oveq2	|- ( B = ( span ` { x } ) -> ( A +H B ) = ( A +H ( span ` { x } ) ) )
4		oveq2	|- ( B = ( span ` { x } ) -> ( A vH B ) = ( A vH ( span ` { x } ) ) )
5	3 4	eqeq12d	|- ( B = ( span ` { x } ) -> ( ( A +H B ) = ( A vH B ) <-> ( A +H ( span ` { x } ) ) = ( A vH ( span ` { x } ) ) ) )
6	2 5	imbitrrid	|- ( B = ( span ` { x } ) -> ( ( A e. CH /\ x e. ~H ) -> ( A +H B ) = ( A vH B ) ) )
7	6	expd	|- ( B = ( span ` { x } ) -> ( A e. CH -> ( x e. ~H -> ( A +H B ) = ( A vH B ) ) ) )
8	7	adantl	|- ( ( x =/= 0h /\ B = ( span ` { x } ) ) -> ( A e. CH -> ( x e. ~H -> ( A +H B ) = ( A vH B ) ) ) )
9	8	com3l	|- ( A e. CH -> ( x e. ~H -> ( ( x =/= 0h /\ B = ( span ` { x } ) ) -> ( A +H B ) = ( A vH B ) ) ) )
10	9	rexlimdv	|- ( A e. CH -> ( E. x e. ~H ( x =/= 0h /\ B = ( span ` { x } ) ) -> ( A +H B ) = ( A vH B ) ) )
11	1 10	biimtrid	|- ( A e. CH -> ( B e. HAtoms -> ( A +H B ) = ( A vH B ) ) )
12	11	imp	|- ( ( A e. CH /\ B e. HAtoms ) -> ( A +H B ) = ( A vH B ) )