Theorem mapdh6N

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 . TODO: If disjoint variable conditions with I and ph become a problem later, use cbv* theorems on I variables here to get rid of them. Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. TODO: may be deleted (with its lemmas), if not needed, in view of hdmap1l6 . (Contributed by NM, 1-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdh6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdh6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdh6.v	$$⊢V={\mathrm{Base}}_U$$
	mapdh6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	mapdh6.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdh6.o	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdh6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdh6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdh6.d	$$⊢D={\mathrm{Base}}_C$$
	mapdh6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	mapdh6.r	$$⊢R={-}_C$$
	mapdh6.q	$$⊢Q=0_C$$
	mapdh6.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdh6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdh6.i	$$⊢I=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
	mapdh6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdh6.f	$$⊢\phi \to F\in D$$
	mapdh6.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh6.y	$$⊢\phi \to Y\in V$$
	mapdh6.z	$$⊢\phi \to Z\in V$$
	mapdh6.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	mapdh6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
Assertion	mapdh6N	$$⊢\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		mapdh6.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdh6.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		mapdh6.v	$$⊢V={\mathrm{Base}}_U$$
4		mapdh6.p	$$⊢\underset{\dot{}}{+}={+}_U$$
5		mapdh6.s	$$⊢\underset{\dot{}}{-}={-}_U$$
6		mapdh6.o	$$⊢\underset{\dot{}}{0}=0_U$$
7		mapdh6.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		mapdh6.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
9		mapdh6.d	$$⊢D={\mathrm{Base}}_C$$
10		mapdh6.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
11		mapdh6.r	$$⊢R={-}_C$$
12		mapdh6.q	$$⊢Q=0_C$$
13		mapdh6.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
14		mapdh6.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
15		mapdh6.i	$$⊢I=\left(x\in \mathrm{V}⟼if\left(2^{nd}\left(x\right)=\underset{\dot{}}{0},Q,\left(\iota h\in D|\left(M\left(N\left(\left\{2^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{h\right\}\right)\wedge M\left(N\left(\left\{1^{st}\left(1^{st}\left(x\right)\right)\underset{\dot{}}{-}{2}^{nd}\left(x\right)\right\}\right)\right)=J\left(\left\{2^{nd}\left(1^{st}\left(x\right)\right)Rh\right\}\right)\right)\right)\right)\right)$$
16		mapdh6.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		mapdh6.f	$$⊢\phi \to F\in D$$
18		mapdh6.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		mapdh6.y	$$⊢\phi \to Y\in V$$
20		mapdh6.z	$$⊢\phi \to Z\in V$$
21		mapdh6.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
22		mapdh6.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
23	12 15 1 14 2 3 5 6 7 8 9 11 13 16 17 22 18 4 10 19 20 21	mapdh6kN	$$⊢\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)$$