Theorem hdmapinvlem2

Description: Line 28 in Baer p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapinvlem1.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
	hdmapinvlem1.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
	hdmapinvlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapinvlem1.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapinvlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapinvlem1.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapinvlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	hdmapinvlem1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	hdmapinvlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapinvlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapinvlem1.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
Assertion	hdmapinvlem2	$$⊢\phi \to S\left(C\right)\left(E\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem1.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapinvlem1.e	$$⊢E=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
3		hdmapinvlem1.o	$$⊢O=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		hdmapinvlem1.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		hdmapinvlem1.v	$$⊢V={\mathrm{Base}}_U$$
6		hdmapinvlem1.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
7		hdmapinvlem1.b	$$⊢B={\mathrm{Base}}_R$$
8		hdmapinvlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
9		hdmapinvlem1.z	$$⊢\underset{\dot{}}{0}=0_R$$
10		hdmapinvlem1.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
11		hdmapinvlem1.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
12		hdmapinvlem1.c	$$⊢\phi \to C\in O\left(\left\{E\right\}\right)$$
13	1 2 3 4 5 6 7 8 9 10 11 12	hdmapinvlem1	$$⊢\phi \to S\left(E\right)\left(C\right)=\underset{\dot{}}{0}$$
14		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
15		eqid	$$⊢\mathrm{LTrn}\left(K\right)\left(W\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
16		eqid	$$⊢0_U=0_U$$
17	1 14 15 4 5 16 2 11	dvheveccl	$$⊢\phi \to E\in \left(V\setminus \left\{0_U\right\}\right)$$
18	17	eldifad	$$⊢\phi \to E\in V$$
19	18	snssd	$$⊢\phi \to \left\{E\right\}\subseteq V$$
20	1 4 5 3	dochssv	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{E\right\}\subseteq V\right)\to O\left(\left\{E\right\}\right)\subseteq V$$
21	11 19 20	syl2anc	$$⊢\phi \to O\left(\left\{E\right\}\right)\subseteq V$$
22	21 12	sseldd	$$⊢\phi \to C\in V$$
23	1 4 5 6 9 10 11 18 22	hdmapip0com	$$⊢\phi \to \left(S\left(E\right)\left(C\right)=\underset{\dot{}}{0}\leftrightarrow S\left(C\right)\left(E\right)=\underset{\dot{}}{0}\right)$$
24	13 23	mpbid	$$⊢\phi \to S\left(C\right)\left(E\right)=\underset{\dot{}}{0}$$