Theorem hdmap14lem9

Description: Part of proof of part 14 in Baer p. 49 line 38. (Contributed by NM, 1-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem8.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap14lem8.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap14lem8.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap14lem8.q	$$⊢\underset{\dot{}}{+}={+}_U$$
	hdmap14lem8.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmap14lem8.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap14lem8.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	hdmap14lem8.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmap14lem8.b	$$⊢B={\mathrm{Base}}_R$$
	hdmap14lem8.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap14lem8.d	$$⊢\underset{\dot{}}{✚}={+}_C$$
	hdmap14lem8.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hdmap14lem8.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
	hdmap14lem8.a	$$⊢A={\mathrm{Base}}_P$$
	hdmap14lem8.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap14lem8.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap14lem8.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap14lem8.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap14lem8.f	$$⊢\phi \to F\in B$$
	hdmap14lem8.g	$$⊢\phi \to G\in A$$
	hdmap14lem8.i	$$⊢\phi \to I\in A$$
	hdmap14lem8.xx	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)=G\underset{\dot{}}{\bullet }S\left(X\right)$$
	hdmap14lem8.yy	$$⊢\phi \to S\left(F\underset{\dot{}}{·}Y\right)=I\underset{\dot{}}{\bullet }S\left(Y\right)$$
	hdmap14lem8.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	hdmap14lem8.j	$$⊢\phi \to J\in A$$
	hdmap14lem8.xy	$$⊢\phi \to S\left(F\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)=J\underset{\dot{}}{\bullet }S\left(X\underset{\dot{}}{+}Y\right)$$
Assertion	hdmap14lem9	$$⊢\phi \to G=I$$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem8.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap14lem8.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap14lem8.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap14lem8.q	$$⊢\underset{\dot{}}{+}={+}_U$$
5		hdmap14lem8.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
6		hdmap14lem8.o	$$⊢\underset{\dot{}}{0}=0_U$$
7		hdmap14lem8.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		hdmap14lem8.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
9		hdmap14lem8.b	$$⊢B={\mathrm{Base}}_R$$
10		hdmap14lem8.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
11		hdmap14lem8.d	$$⊢\underset{\dot{}}{✚}={+}_C$$
12		hdmap14lem8.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
13		hdmap14lem8.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
14		hdmap14lem8.a	$$⊢A={\mathrm{Base}}_P$$
15		hdmap14lem8.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
16		hdmap14lem8.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		hdmap14lem8.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		hdmap14lem8.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
19		hdmap14lem8.f	$$⊢\phi \to F\in B$$
20		hdmap14lem8.g	$$⊢\phi \to G\in A$$
21		hdmap14lem8.i	$$⊢\phi \to I\in A$$
22		hdmap14lem8.xx	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)=G\underset{\dot{}}{\bullet }S\left(X\right)$$
23		hdmap14lem8.yy	$$⊢\phi \to S\left(F\underset{\dot{}}{·}Y\right)=I\underset{\dot{}}{\bullet }S\left(Y\right)$$
24		hdmap14lem8.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
25		hdmap14lem8.j	$$⊢\phi \to J\in A$$
26		hdmap14lem8.xy	$$⊢\phi \to S\left(F\underset{\dot{}}{·}\left(X\underset{\dot{}}{+}Y\right)\right)=J\underset{\dot{}}{\bullet }S\left(X\underset{\dot{}}{+}Y\right)$$
27		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
28		eqid	$$⊢0_C=0_C$$
29		eqid	$$⊢\mathrm{LSpan}\left(C\right)=\mathrm{LSpan}\left(C\right)$$
30	1 10 16	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
31	1 2 3 6 10 28 27 15 16 17	hdmapnzcl	$$⊢\phi \to S\left(X\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)$$
32	1 2 3 6 10 28 27 15 16 18	hdmapnzcl	$$⊢\phi \to S\left(Y\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)$$
33		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
34		eqid	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
35	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
36	17	eldifad	$$⊢\phi \to X\in V$$
37	3 33 7	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
38	35 36 37	syl2anc	$$⊢\phi \to N\left(\left\{X\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
39	18	eldifad	$$⊢\phi \to Y\in V$$
40	3 33 7	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge Y\in V\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
41	35 39 40	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
42	1 2 33 34 16 38 41	mapd11	$$⊢\phi \to \left(\mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{X\right\}\right)\right)=\mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{Y\right\}\right)\right)\leftrightarrow N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)\right)$$
43	42	necon3bid	$$⊢\phi \to \left(\mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{X\right\}\right)\right)\ne \mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{Y\right\}\right)\right)\leftrightarrow N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)\right)$$
44	24 43	mpbird	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{X\right\}\right)\right)\ne \mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{Y\right\}\right)\right)$$
45	1 2 3 7 10 29 34 15 16 36	hdmap10	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{X\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{S\left(X\right)\right\}\right)$$
46	1 2 3 7 10 29 34 15 16 39	hdmap10	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(N\left(\left\{Y\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{S\left(Y\right)\right\}\right)$$
47	44 45 46	3netr3d	$$⊢\phi \to \mathrm{LSpan}\left(C\right)\left(\left\{S\left(X\right)\right\}\right)\ne \mathrm{LSpan}\left(C\right)\left(\left\{S\left(Y\right)\right\}\right)$$
48	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 26	hdmap14lem8	$$⊢\phi \to \left(J\underset{\dot{}}{\bullet }S\left(X\right)\right)\underset{\dot{}}{✚}\left(J\underset{\dot{}}{\bullet }S\left(Y\right)\right)=\left(G\underset{\dot{}}{\bullet }S\left(X\right)\right)\underset{\dot{}}{✚}\left(I\underset{\dot{}}{\bullet }S\left(Y\right)\right)$$
49	27 11 13 14 12 28 29 30 31 32 25 25 20 21 47 48	lvecindp2	$$⊢\phi \to \left(J=G\wedge J=I\right)$$
50	49	simpld	$$⊢\phi \to J=G$$
51	49	simprd	$$⊢\phi \to J=I$$
52	50 51	eqtr3d	$$⊢\phi \to G=I$$