Theorem hdmap14lem6

Description: Case where F is zero. (Contributed by NM, 1-Jun-2015)

	Ref	Expression
Hypotheses	hdmap14lem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap14lem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap14lem1.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap14lem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hdmap14lem3.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap14lem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmap14lem1.b	$$⊢B={\mathrm{Base}}_R$$
	hdmap14lem1.z	$$⊢Z=0_R$$
	hdmap14lem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap14lem2.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hdmap14lem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
	hdmap14lem2.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
	hdmap14lem2.a	$$⊢A={\mathrm{Base}}_P$$
	hdmap14lem2.q	$$⊢Q=0_P$$
	hdmap14lem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap14lem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap14lem3.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	hdmap14lem6.f	$$⊢\phi \to F=Z$$
Assertion	hdmap14lem6	$$⊢\phi \to \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap14lem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap14lem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap14lem1.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap14lem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hdmap14lem3.o	$$⊢\underset{\dot{}}{0}=0_U$$
6		hdmap14lem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
7		hdmap14lem1.b	$$⊢B={\mathrm{Base}}_R$$
8		hdmap14lem1.z	$$⊢Z=0_R$$
9		hdmap14lem1.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
10		hdmap14lem2.e	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
11		hdmap14lem1.l	$$⊢L=\mathrm{LSpan}\left(C\right)$$
12		hdmap14lem2.p	$$⊢P=\mathrm{Scalar}\left(C\right)$$
13		hdmap14lem2.a	$$⊢A={\mathrm{Base}}_P$$
14		hdmap14lem2.q	$$⊢Q=0_P$$
15		hdmap14lem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
16		hdmap14lem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17		hdmap14lem3.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
18		hdmap14lem6.f	$$⊢\phi \to F=Z$$
19	1 9 16	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
20	12 13 14	lmod0cl	$$⊢C\in \mathrm{LMod}\to Q\in A$$
21	19 20	syl	$$⊢\phi \to Q\in A$$
22		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
23	17	eldifad	$$⊢\phi \to X\in V$$
24	1 2 3 9 22 15 16 23	hdmapcl	$$⊢\phi \to S\left(X\right)\in {\mathrm{Base}}_C$$
25		eqid	$$⊢0_C=0_C$$
26	22 12 10 14 25	lmod0vs	$$⊢\left(C\in \mathrm{LMod}\wedge S\left(X\right)\in {\mathrm{Base}}_C\right)\to Q\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
27	19 24 26	syl2anc	$$⊢\phi \to Q\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
28	27	eqcomd	$$⊢\phi \to 0_C=Q\underset{\dot{}}{\bullet }S\left(X\right)$$
29		oveq1	$$⊢g=Q\to g\underset{\dot{}}{\bullet }S\left(X\right)=Q\underset{\dot{}}{\bullet }S\left(X\right)$$
30	29	rspceeqv	$$⊢\left(Q\in A\wedge 0_C=Q\underset{\dot{}}{\bullet }S\left(X\right)\right)\to \exists g\in A{0}_C=g\underset{\dot{}}{\bullet }S\left(X\right)$$
31	21 28 30	syl2anc	$$⊢\phi \to \exists g\in A{0}_C=g\underset{\dot{}}{\bullet }S\left(X\right)$$
32	1 2 3 5 9 25 22 15 16 17	hdmapnzcl	$$⊢\phi \to S\left(X\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)$$
33		eldifsni	$$⊢S\left(X\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)\to S\left(X\right)\ne 0_C$$
34	32 33	syl	$$⊢\phi \to S\left(X\right)\ne 0_C$$
35	34	neneqd	$$⊢\phi \to \neg S\left(X\right)=0_C$$
36	35	3ad2ant1	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \neg S\left(X\right)=0_C$$
37		simp3l	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to 0_C=g\underset{\dot{}}{\bullet }S\left(X\right)$$
38	37	eqcomd	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to g\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
39	1 9 16	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
40	39	3ad2ant1	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to C\in \mathrm{LVec}$$
41		simp2l	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to g\in A$$
42	24	3ad2ant1	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to S\left(X\right)\in {\mathrm{Base}}_C$$
43	22 10 12 13 14 25 40 41 42	lvecvs0or	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(g\underset{\dot{}}{\bullet }S\left(X\right)=0_C\leftrightarrow \left(g=Q\vee S\left(X\right)=0_C\right)\right)$$
44	38 43	mpbid	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(g=Q\vee S\left(X\right)=0_C\right)$$
45	44	orcomd	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(S\left(X\right)=0_C\vee g=Q\right)$$
46	45	ord	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(\neg S\left(X\right)=0_C\to g=Q\right)$$
47	36 46	mpd	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to g=Q$$
48		simp3r	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)$$
49	48	eqcomd	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to h\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
50		simp2r	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to h\in A$$
51	22 10 12 13 14 25 40 50 42	lvecvs0or	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(h\underset{\dot{}}{\bullet }S\left(X\right)=0_C\leftrightarrow \left(h=Q\vee S\left(X\right)=0_C\right)\right)$$
52	49 51	mpbid	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(h=Q\vee S\left(X\right)=0_C\right)$$
53	52	orcomd	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(S\left(X\right)=0_C\vee h=Q\right)$$
54	53	ord	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to \left(\neg S\left(X\right)=0_C\to h=Q\right)$$
55	36 54	mpd	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to h=Q$$
56	47 55	eqtr4d	$$⊢\left(\phi \wedge \left(g\in A\wedge h\in A\right)\wedge \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\right)\to g=h$$
57	56	3exp	$$⊢\phi \to \left(\left(g\in A\wedge h\in A\right)\to \left(\left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\to g=h\right)\right)$$
58	57	ralrimivv	$$⊢\phi \to \forall g\in A\forall h\in A\left(\left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\to g=h\right)$$
59		oveq1	$$⊢g=h\to g\underset{\dot{}}{\bullet }S\left(X\right)=h\underset{\dot{}}{\bullet }S\left(X\right)$$
60	59	eqeq2d	$$⊢g=h\to \left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
61	60	reu4	$$⊢\exists !g\in A{0}_C=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \left(\exists g\in A{0}_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge \forall g\in A\forall h\in A\left(\left(0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\wedge 0_C=h\underset{\dot{}}{\bullet }S\left(X\right)\right)\to g=h\right)\right)$$
62	31 58 61	sylanbrc	$$⊢\phi \to \exists !g\in A{0}_C=g\underset{\dot{}}{\bullet }S\left(X\right)$$
63	18	oveq1d	$$⊢\phi \to F\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}X$$
64	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
65	3 6 4 8 5	lmod0vs	$$⊢\left(U\in \mathrm{LMod}\wedge X\in V\right)\to Z\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
66	64 23 65	syl2anc	$$⊢\phi \to Z\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
67	63 66	eqtrd	$$⊢\phi \to F\underset{\dot{}}{·}X=\underset{\dot{}}{0}$$
68	67	fveq2d	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)=S\left(\underset{\dot{}}{0}\right)$$
69	1 2 5 9 25 15 16	hdmapval0	$$⊢\phi \to S\left(\underset{\dot{}}{0}\right)=0_C$$
70	68 69	eqtrd	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)=0_C$$
71	70	eqeq1d	$$⊢\phi \to \left(S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow 0_C=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
72	71	reubidv	$$⊢\phi \to \left(\exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists !g\in A{0}_C=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
73	62 72	mpbird	$$⊢\phi \to \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$