Theorem mapdh6gN

Description: Lemmma for mapdh6N . Part (6) of Baer p. 47 line 39. (Contributed by NM, 1-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mapdh.q	$$⊢Q=0_C$$
	mapdh.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)$$
	mapdh.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdh.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdh.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdh.v	$$⊢V={\mathrm{Base}}_U$$
	mapdh.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdhc.o	$$⊢\underset{\dot{}}{0}=0_U$$
	mapdh.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdh.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdh.d	$$⊢D={\mathrm{Base}}_C$$
	mapdh.r	$$⊢R={-}_C$$
	mapdh.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdh.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdhc.f	$$⊢\phi \to F\in D$$
	mapdh.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
	mapdhcl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	mapdh.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
	mapdh6d.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
	mapdh6d.yz	$$⊢\phi \to N\left(\left\{Y\right\}\right)=N\left(\left\{Z\right\}\right)$$
	mapdh6d.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh6d.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh6d.w	$$⊢\phi \to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	mapdh6d.wn	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\right\}\right)$$
Assertion	mapdh6gN	$$⊢\phi \to I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=\left(I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y⟩\right)\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	$$⊢Q=0_C$$
2		mapdh.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)$$
3		mapdh.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
4		mapdh.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
5		mapdh.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
6		mapdh.v	$$⊢V={\mathrm{Base}}_U$$
7		mapdh.s	$$⊢\underset{\dot{}}{-}={-}_U$$
8		mapdhc.o	$$⊢\underset{\dot{}}{0}=0_U$$
9		mapdh.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
10		mapdh.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
11		mapdh.d	$$⊢D={\mathrm{Base}}_C$$
12		mapdh.r	$$⊢R={-}_C$$
13		mapdh.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
14		mapdh.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
15		mapdhc.f	$$⊢\phi \to F\in D$$
16		mapdh.mn	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{F\right\}\right)$$
17		mapdhcl.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		mapdh.p	$$⊢\underset{\dot{}}{+}={+}_U$$
19		mapdh.a	$$⊢\underset{\dot{}}{✚}={+}_C$$
20		mapdh6d.xn	$$⊢\phi \to \neg X\in N\left(\left\{Y,Z\right\}\right)$$
21		mapdh6d.yz	$$⊢\phi \to N\left(\left\{Y\right\}\right)=N\left(\left\{Z\right\}\right)$$
22		mapdh6d.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
23		mapdh6d.z	$$⊢\phi \to Z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
24		mapdh6d.w	$$⊢\phi \to w\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
25		mapdh6d.wn	$$⊢\phi \to \neg w\in N\left(\left\{X,Y\right\}\right)$$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	mapdh6dN	$$⊢\phi \to I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)=I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)$$
27	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	mapdh6eN	$$⊢\phi \to I\left(⟨X,F,\left(w\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,w\underset{\dot{}}{+}Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$
28	3 5 14	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
29	24	eldifad	$$⊢\phi \to w\in V$$
30	22	eldifad	$$⊢\phi \to Y\in V$$
31	23	eldifad	$$⊢\phi \to Z\in V$$
32	6 18	lmodass	$$⊢\left(U\in \mathrm{LMod}\wedge \left(w\in V\wedge Y\in V\wedge Z\in V\right)\right)\to \left(w\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
33	28 29 30 31 32	syl13anc	$$⊢\phi \to \left(w\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z=w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)$$
34	33	oteq3d	$$⊢\phi \to ⟨X,F,\left(w\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z⟩=⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩$$
35	34	fveq2d	$$⊢\phi \to I\left(⟨X,F,\left(w\underset{\dot{}}{+}Y\right)\underset{\dot{}}{+}Z⟩\right)=I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)$$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25	mapdh6fN	$$⊢\phi \to I\left(⟨X,F,w\underset{\dot{}}{+}Y⟩\right)=I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y⟩\right)$$
37	36	oveq1d	$$⊢\phi \to I\left(⟨X,F,w\underset{\dot{}}{+}Y⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)=\left(I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y⟩\right)\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$
38	27 35 37	3eqtr3d	$$⊢\phi \to I\left(⟨X,F,w\underset{\dot{}}{+}\left(Y\underset{\dot{}}{+}Z\right)⟩\right)=\left(I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y⟩\right)\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$
39	26 38	eqtr3d	$$⊢\phi \to I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y\underset{\dot{}}{+}Z⟩\right)=\left(I\left(⟨X,F,w⟩\right)\underset{\dot{}}{✚}I\left(⟨X,F,Y⟩\right)\right)\underset{\dot{}}{✚}I\left(⟨X,F,Z⟩\right)$$