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	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		atom1d	$$⊢B\in \mathrm{HAtoms}\leftrightarrow \exists x\in \mathscr{H}\left(x\ne 0_{ℎ}\wedge B=\mathrm{span}\left(\left\{x\right\}\right)\right)$$
2		spansnj	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in \mathscr{H}\right)\to A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{x\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{x\right\}\right)$$
3		oveq2	$$⊢B=\mathrm{span}\left(\left\{x\right\}\right)\to A{+}_{\mathscr{H}}B=A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{x\right\}\right)$$
4		oveq2	$$⊢B=\mathrm{span}\left(\left\{x\right\}\right)\to A{\vee }_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{x\right\}\right)$$
5	3 4	eqeq12d	$$⊢B=\mathrm{span}\left(\left\{x\right\}\right)\to \left(A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\leftrightarrow A{+}_{\mathscr{H}}\mathrm{span}\left(\left\{x\right\}\right)=A{\vee }_{\mathscr{H}}\mathrm{span}\left(\left\{x\right\}\right)\right)$$
6	2 5	imbitrrid	$$⊢B=\mathrm{span}\left(\left\{x\right\}\right)\to \left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in \mathscr{H}\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)$$
7	6	expd	$$⊢B=\mathrm{span}\left(\left\{x\right\}\right)\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\in \mathscr{H}\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)\right)$$
8	7	adantl	$$⊢\left(x\ne 0_{ℎ}\wedge B=\mathrm{span}\left(\left\{x\right\}\right)\right)\to \left(A\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\in \mathscr{H}\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)\right)$$
9	8	com3l	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\in \mathscr{H}\to \left(\left(x\ne 0_{ℎ}\wedge B=\mathrm{span}\left(\left\{x\right\}\right)\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)\right)$$
10	9	rexlimdv	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\exists x\in \mathscr{H}\left(x\ne 0_{ℎ}\wedge B=\mathrm{span}\left(\left\{x\right\}\right)\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)$$
11	1 10	biimtrid	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(B\in \mathrm{HAtoms}\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)$$
12	11	imp	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in \mathrm{HAtoms}\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$