Theorem baerlem5b

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. Second equation of part (5) in Baer p. 46. (Contributed by NM, 13-Apr-2015)

	Ref	Expression
Hypotheses	baerlem3.v	$$⊢V={\mathrm{Base}}_W$$
	baerlem3.m	$$⊢\underset{\dot{}}{-}={-}_W$$
	baerlem3.o	$$⊢\underset{\dot{}}{0}=0_W$$
	baerlem3.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	baerlem3.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	baerlem3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	baerlem3.x	$$⊢\phi \to X\in V$$
	baerlem3.c	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	baerlem3.d	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
	baerlem3.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	baerlem3.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	baerlem5a.p	$$⊢\underset{\dot{}}{+}={+}_W$$
Assertion	baerlem5b	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)=\left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		baerlem3.v	$$⊢V={\mathrm{Base}}_W$$
2		baerlem3.m	$$⊢\underset{\dot{}}{-}={-}_W$$
3		baerlem3.o	$$⊢\underset{\dot{}}{0}=0_W$$
4		baerlem3.s	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
5		baerlem3.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
6		baerlem3.w	$$⊢\phi \to W\in \mathrm{LVec}$$
7		baerlem3.x	$$⊢\phi \to X\in V$$
8		baerlem3.c	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
9		baerlem3.d	$$⊢\phi \to N\left(\left\{Y\right\}\right)\ne N\left(\left\{Z\right\}\right)$$
10		baerlem3.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		baerlem3.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		baerlem5a.p	$$⊢\underset{\dot{}}{+}={+}_W$$
13		eqid	$$⊢{\cdot }_W={\cdot }_W$$
14		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
16		eqid	$$⊢{+}_{\mathrm{Scalar}\left(W\right)}={+}_{\mathrm{Scalar}\left(W\right)}$$
17		eqid	$$⊢{-}_{\mathrm{Scalar}\left(W\right)}={-}_{\mathrm{Scalar}\left(W\right)}$$
18		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
19		eqid	$$⊢{inv}_g\left(\mathrm{Scalar}\left(W\right)\right)={inv}_g\left(\mathrm{Scalar}\left(W\right)\right)$$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	baerlem5blem2	$$⊢\phi \to N\left(\left\{Y\underset{\dot{}}{+}Z\right\}\right)=\left(N\left(\left\{Y\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{Z\right\}\right)\right)\cap \left(N\left(\left\{X\underset{\dot{}}{-}\left(Y\underset{\dot{}}{+}Z\right)\right\}\right)\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)\right)$$