Theorem hdmapeq0

Description: Part of proof of part 12 in Baer p. 49 line 3. (Contributed by NM, 22-May-2015)

	Ref	Expression
Hypotheses	hdmap12a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmap12a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap12a.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap12a.o	$$⊢\underset{\dot{}}{0}=0_U$$
	hdmap12a.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap12a.q	$$⊢Q=0_C$$
	hdmap12a.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap12a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap12a.x	$$⊢\phi \to T\in V$$
Assertion	hdmapeq0	$$⊢\phi \to \left(S\left(T\right)=Q\leftrightarrow T=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap12a.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap12a.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap12a.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap12a.o	$$⊢\underset{\dot{}}{0}=0_U$$
5		hdmap12a.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmap12a.q	$$⊢Q=0_C$$
7		hdmap12a.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
8		hdmap12a.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hdmap12a.x	$$⊢\phi \to T\in V$$
10		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
11		eqid	$$⊢\mathrm{LSpan}\left(C\right)=\mathrm{LSpan}\left(C\right)$$
12		eqid	$$⊢\mathrm{mapd}\left(K\right)\left(W\right)=\mathrm{mapd}\left(K\right)\left(W\right)$$
13	1 2 3 10 5 11 12 7 8 9	hdmap10	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)\right)=\mathrm{LSpan}\left(C\right)\left(\left\{S\left(T\right)\right\}\right)$$
14	1 12 2 4 5 6 8	mapd0	$$⊢\phi \to \mathrm{mapd}\left(K\right)\left(W\right)\left(\left\{\underset{\dot{}}{0}\right\}\right)=\left\{Q\right\}$$
15	13 14	eqeq12d	$$⊢\phi \to \left(\mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)\right)=\mathrm{mapd}\left(K\right)\left(W\right)\left(\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \mathrm{LSpan}\left(C\right)\left(\left\{S\left(T\right)\right\}\right)=\left\{Q\right\}\right)$$
16		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
17	1 2 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18	3 16 10	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge T\in V\right)\to \mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
19	17 9 18	syl2anc	$$⊢\phi \to \mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
20	4 16	lsssn0	$$⊢U\in \mathrm{LMod}\to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(U\right)$$
21	17 20	syl	$$⊢\phi \to \left\{\underset{\dot{}}{0}\right\}\in \mathrm{LSubSp}\left(U\right)$$
22	1 2 16 12 8 19 21	mapd11	$$⊢\phi \to \left(\mathrm{mapd}\left(K\right)\left(W\right)\left(\mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)\right)=\mathrm{mapd}\left(K\right)\left(W\right)\left(\left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
23	1 5 8	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
24		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
25	1 2 3 5 24 7 8 9	hdmapcl	$$⊢\phi \to S\left(T\right)\in {\mathrm{Base}}_C$$
26	24 6 11	lspsneq0	$$⊢\left(C\in \mathrm{LMod}\wedge S\left(T\right)\in {\mathrm{Base}}_C\right)\to \left(\mathrm{LSpan}\left(C\right)\left(\left\{S\left(T\right)\right\}\right)=\left\{Q\right\}\leftrightarrow S\left(T\right)=Q\right)$$
27	23 25 26	syl2anc	$$⊢\phi \to \left(\mathrm{LSpan}\left(C\right)\left(\left\{S\left(T\right)\right\}\right)=\left\{Q\right\}\leftrightarrow S\left(T\right)=Q\right)$$
28	15 22 27	3bitr3rd	$$⊢\phi \to \left(S\left(T\right)=Q\leftrightarrow \mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
29	3 4 10	lspsneq0	$$⊢\left(U\in \mathrm{LMod}\wedge T\in V\right)\to \left(\mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow T=\underset{\dot{}}{0}\right)$$
30	17 9 29	syl2anc	$$⊢\phi \to \left(\mathrm{LSpan}\left(U\right)\left(\left\{T\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow T=\underset{\dot{}}{0}\right)$$
31	28 30	bitrd	$$⊢\phi \to \left(S\left(T\right)=Q\leftrightarrow T=\underset{\dot{}}{0}\right)$$