Theorem hdmap14lem4a

Description: Simplify ( A \ { Q } ) in hdmap14lem3 to provide a slightly simpler definition later. (Contributed by NM, 31-May-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)$$
	hdmap14lem1.f	$$⊢\phi \to F\in \left(B\setminus \left\{Z\right\}\right)$$
Assertion	hdmap14lem4a	$$⊢\phi \to \left(\exists !g\in \left(A\setminus \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\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		hdmap14lem1.f	$$⊢\phi \to F\in \left(B\setminus \left\{Z\right\}\right)$$
19		eqid	$$⊢0_C=0_C$$
20		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
21	1 2 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
22	18	eldifad	$$⊢\phi \to F\in B$$
23	17	eldifad	$$⊢\phi \to X\in V$$
24	3 6 4 7	lmodvscl	$$⊢\left(U\in \mathrm{LMod}\wedge F\in B\wedge X\in V\right)\to F\underset{\dot{}}{·}X\in V$$
25	21 22 23 24	syl3anc	$$⊢\phi \to F\underset{\dot{}}{·}X\in V$$
26		eldifsni	$$⊢F\in \left(B\setminus \left\{Z\right\}\right)\to F\ne Z$$
27	18 26	syl	$$⊢\phi \to F\ne Z$$
28		eldifsni	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
29	17 28	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
30	1 2 16	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
31	3 4 6 7 8 5 30 22 23	lvecvsn0	$$⊢\phi \to \left(F\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}\leftrightarrow \left(F\ne Z\wedge X\ne \underset{\dot{}}{0}\right)\right)$$
32	27 29 31	mpbir2and	$$⊢\phi \to F\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}$$
33		eldifsn	$$⊢F\underset{\dot{}}{·}X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(F\underset{\dot{}}{·}X\in V\wedge F\underset{\dot{}}{·}X\ne \underset{\dot{}}{0}\right)$$
34	25 32 33	sylanbrc	$$⊢\phi \to F\underset{\dot{}}{·}X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
35	1 2 3 5 9 19 20 15 16 34	hdmapnzcl	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)$$
36		eldifsni	$$⊢S\left(F\underset{\dot{}}{·}X\right)\in \left({\mathrm{Base}}_C\setminus \left\{0_C\right\}\right)\to S\left(F\underset{\dot{}}{·}X\right)\ne 0_C$$
37	35 36	syl	$$⊢\phi \to S\left(F\underset{\dot{}}{·}X\right)\ne 0_C$$
38	37	adantr	$$⊢\left(\phi \wedge g\in \left\{Q\right\}\right)\to S\left(F\underset{\dot{}}{·}X\right)\ne 0_C$$
39		elsni	$$⊢g\in \left\{Q\right\}\to g=Q$$
40	39	oveq1d	$$⊢g\in \left\{Q\right\}\to g\underset{\dot{}}{\bullet }S\left(X\right)=Q\underset{\dot{}}{\bullet }S\left(X\right)$$
41	1 9 16	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
42	1 2 3 9 20 15 16 23	hdmapcl	$$⊢\phi \to S\left(X\right)\in {\mathrm{Base}}_C$$
43	20 12 10 14 19	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$$
44	41 42 43	syl2anc	$$⊢\phi \to Q\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
45	40 44	sylan9eqr	$$⊢\left(\phi \wedge g\in \left\{Q\right\}\right)\to g\underset{\dot{}}{\bullet }S\left(X\right)=0_C$$
46	38 45	neeqtrrd	$$⊢\left(\phi \wedge g\in \left\{Q\right\}\right)\to S\left(F\underset{\dot{}}{·}X\right)\ne g\underset{\dot{}}{\bullet }S\left(X\right)$$
47	46	neneqd	$$⊢\left(\phi \wedge g\in \left\{Q\right\}\right)\to \neg S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$
48	47	nrexdv	$$⊢\phi \to \neg \exists g\in \left\{Q\right\}S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)$$
49		reuun2	$$⊢\neg \exists g\in \left\{Q\right\}S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\to \left(\exists !g\in \left(\left(A\setminus \left\{Q\right\}\right)\cup \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists !g\in \left(A\setminus \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
50	48 49	syl	$$⊢\phi \to \left(\exists !g\in \left(\left(A\setminus \left\{Q\right\}\right)\cup \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists !g\in \left(A\setminus \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
51	12 13 14	lmod0cl	$$⊢C\in \mathrm{LMod}\to Q\in A$$
52		difsnid	$$⊢Q\in A\to \left(A\setminus \left\{Q\right\}\right)\cup \left\{Q\right\}=A$$
53		reueq1	$$⊢\left(A\setminus \left\{Q\right\}\right)\cup \left\{Q\right\}=A\to \left(\exists !g\in \left(\left(A\setminus \left\{Q\right\}\right)\cup \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
54	41 51 52 53	4syl	$$⊢\phi \to \left(\exists !g\in \left(\left(A\setminus \left\{Q\right\}\right)\cup \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$
55	50 54	bitr3d	$$⊢\phi \to \left(\exists !g\in \left(A\setminus \left\{Q\right\}\right)S\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\leftrightarrow \exists !g\in AS\left(F\underset{\dot{}}{·}X\right)=g\underset{\dot{}}{\bullet }S\left(X\right)\right)$$