Theorem hdmap1l6

Description: Part (6) of Baer p. 47 line 6. Note that we use -. X e. ( N{ Y , Z } ) which is equivalent to Baer's "Fx i^i (Fy + Fz)" by lspdisjb . (Convert mapdh6N to use the function HDMap1 .) (Contributed by NM, 17-May-2015)

	Ref	Expression
Hypotheses	hdmap1-6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap1-6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap1-6.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap1-6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmap1-6.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap1-6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap1-6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap1-6.d	$$⊢D={\mathrm{Base}}_C$$
	hdmap1-6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	hdmap1-6.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmap1-6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	hdmap1-6.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
	hdmap1-6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap1-6.f	$$⊢\phi \to F\in D$$
	hdmap1-6.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap1-6.y	$$⊢\phi \to Y\in V$$
	hdmap1-6.z	$$⊢\phi \to Z\in V$$
	hdmap1-6.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	hdmap1-6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
Assertion	hdmap1l6	$$⊢\phi \to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap1-6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap1-6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap1-6.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap1-6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		hdmap1-6.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmap1-6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		hdmap1-6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hdmap1-6.d	$$⊢D={\mathrm{Base}}_C$$
9		hdmap1-6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
10		hdmap1-6.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
11		hdmap1-6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
12		hdmap1-6.i	$$⊢I=\mathrm{HDMap1}\left(K\right)\left(W\right)$$
13		hdmap1-6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
14		hdmap1-6.f	$$⊢\phi \to F\in D$$
15		hdmap1-6.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
16		hdmap1-6.y	$$⊢\phi \to Y\in V$$
17		hdmap1-6.z	$$⊢\phi \to Z\in V$$
18		hdmap1-6.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
19		hdmap1-6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=L\left(\left\{F\right\}\right)$$
20		eqid	$$⊢{-}_U={-}_U$$
21		eqid	$$⊢{-}_C={-}_C$$
22		eqid	$$⊢0_C=0_C$$
23	1 2 3 4 20 5 6 7 8 9 21 22 10 11 12 13 14 15 19 16 17 18	hdmap1l6k	$$⊢\phi \to I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$