Theorem spansnm0i

Description: The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	spansnm0.1	$$⊢A\in \mathscr{H}$$
	spansnm0.2	$$⊢B\in \mathscr{H}$$
Assertion	spansnm0i	$$⊢\neg A\in \mathrm{span}\left(\left\{B\right\}\right)\to \mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)=0_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		spansnm0.1	$$⊢A\in \mathscr{H}$$
2		spansnm0.2	$$⊢B\in \mathscr{H}$$
3	2	spansnchi	$$⊢\mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	chshii	$$⊢\mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
5		elspansn5	$$⊢\mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{S}}_{\mathscr{H}}\to \left(\left(\left(A\in \mathscr{H}\wedge \neg A\in \mathrm{span}\left(\left\{B\right\}\right)\right)\wedge \left(x\in \mathrm{span}\left(\left\{A\right\}\right)\wedge x\in \mathrm{span}\left(\left\{B\right\}\right)\right)\right)\to x=0_{ℎ}\right)$$
6	4 5	ax-mp	$$⊢\left(\left(A\in \mathscr{H}\wedge \neg A\in \mathrm{span}\left(\left\{B\right\}\right)\right)\wedge \left(x\in \mathrm{span}\left(\left\{A\right\}\right)\wedge x\in \mathrm{span}\left(\left\{B\right\}\right)\right)\right)\to x=0_{ℎ}$$
7	1 6	mpanl1	$$⊢\left(\neg A\in \mathrm{span}\left(\left\{B\right\}\right)\wedge \left(x\in \mathrm{span}\left(\left\{A\right\}\right)\wedge x\in \mathrm{span}\left(\left\{B\right\}\right)\right)\right)\to x=0_{ℎ}$$
8	7	ex	$$⊢\neg A\in \mathrm{span}\left(\left\{B\right\}\right)\to \left(\left(x\in \mathrm{span}\left(\left\{A\right\}\right)\wedge x\in \mathrm{span}\left(\left\{B\right\}\right)\right)\to x=0_{ℎ}\right)$$
9		elin	$$⊢x\in \left(\mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)\right)\leftrightarrow \left(x\in \mathrm{span}\left(\left\{A\right\}\right)\wedge x\in \mathrm{span}\left(\left\{B\right\}\right)\right)$$
10		elch0	$$⊢x\in 0_{\mathscr{H}}\leftrightarrow x=0_{ℎ}$$
11	8 9 10	3imtr4g	$$⊢\neg A\in \mathrm{span}\left(\left\{B\right\}\right)\to \left(x\in \left(\mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)\right)\to x\in 0_{\mathscr{H}}\right)$$
12	11	ssrdv	$$⊢\neg A\in \mathrm{span}\left(\left\{B\right\}\right)\to \mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)\subseteq 0_{\mathscr{H}}$$
13	1	spansnchi	$$⊢\mathrm{span}\left(\left\{A\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
14	13 3	chincli	$$⊢\mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	14	chle0i	$$⊢\mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)\subseteq 0_{\mathscr{H}}\leftrightarrow \mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)=0_{\mathscr{H}}$$
16	12 15	sylib	$$⊢\neg A\in \mathrm{span}\left(\left\{B\right\}\right)\to \mathrm{span}\left(\left\{A\right\}\right)\cap \mathrm{span}\left(\left\{B\right\}\right)=0_{\mathscr{H}}$$