Theorem lclkrlem2l

Description: Lemma for lclkr . Eliminate the X =/= .0. , Y =/= .0. hypotheses. (Contributed by NM, 18-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2f.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lclkrlem2f.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lclkrlem2f.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lclkrlem2f.v	$$⊢V={\mathrm{Base}}_U$$
	lclkrlem2f.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lclkrlem2f.q	$$⊢Q=0_S$$
	lclkrlem2f.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lclkrlem2f.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	lclkrlem2f.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lclkrlem2f.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lclkrlem2f.j	$$⊢J=\mathrm{LSHyp}\left(U\right)$$
	lclkrlem2f.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lclkrlem2f.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lclkrlem2f.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	lclkrlem2f.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lclkrlem2f.b	$$⊢\phi \to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lclkrlem2f.e	$$⊢\phi \to E\in F$$
	lclkrlem2f.g	$$⊢\phi \to G\in F$$
	lclkrlem2f.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
	lclkrlem2f.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
	lclkrlem2f.kb	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(B\right)=Q$$
	lclkrlem2f.nx	$$⊢\phi \to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
	lclkrlem2l.x	$$⊢\phi \to X\in V$$
	lclkrlem2l.y	$$⊢\phi \to Y\in V$$
Assertion	lclkrlem2l	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)$$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2f.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lclkrlem2f.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lclkrlem2f.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lclkrlem2f.v	$$⊢V={\mathrm{Base}}_U$$
5		lclkrlem2f.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
6		lclkrlem2f.q	$$⊢Q=0_S$$
7		lclkrlem2f.z	$$⊢\underset{\dot{}}{0}=0_U$$
8		lclkrlem2f.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
9		lclkrlem2f.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
10		lclkrlem2f.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
11		lclkrlem2f.j	$$⊢J=\mathrm{LSHyp}\left(U\right)$$
12		lclkrlem2f.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
13		lclkrlem2f.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
14		lclkrlem2f.p	$$⊢\underset{\dot{}}{+}={+}_D$$
15		lclkrlem2f.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
16		lclkrlem2f.b	$$⊢\phi \to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
17		lclkrlem2f.e	$$⊢\phi \to E\in F$$
18		lclkrlem2f.g	$$⊢\phi \to G\in F$$
19		lclkrlem2f.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
20		lclkrlem2f.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
21		lclkrlem2f.kb	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(B\right)=Q$$
22		lclkrlem2f.nx	$$⊢\phi \to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
23		lclkrlem2l.x	$$⊢\phi \to X\in V$$
24		lclkrlem2l.y	$$⊢\phi \to Y\in V$$
25	15	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
26	16	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
27	17	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to E\in F$$
28	18	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to G\in F$$
29	19	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
30	20	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
31	21	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to \left(E\underset{\dot{}}{+}G\right)\left(B\right)=Q$$
32	22	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
33		simpr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to X=\underset{\dot{}}{0}$$
34	24	adantr	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to Y\in V$$
35	1 2 3 4 5 6 7 8 9 10 11 12 13 14 25 26 27 28 29 30 31 32 33 34	lclkrlem2k	$$⊢\left(\phi \wedge X=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)$$
36	15	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
37	16	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
38	17	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to E\in F$$
39	18	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to G\in F$$
40	19	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
41	20	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
42	21	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to \left(E\underset{\dot{}}{+}G\right)\left(B\right)=Q$$
43	22	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
44	23	adantr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to X\in V$$
45		simpr	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to Y=\underset{\dot{}}{0}$$
46	1 2 3 4 5 6 7 8 9 10 11 12 13 14 36 37 38 39 40 41 42 43 44 45	lclkrlem2j	$$⊢\left(\phi \wedge Y=\underset{\dot{}}{0}\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)$$
47	15	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
48	16	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to B\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
49	17	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to E\in F$$
50	18	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to G\in F$$
51	19	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
52	20	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
53	21	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to \left(E\underset{\dot{}}{+}G\right)\left(B\right)=Q$$
54	22	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to \left(\neg X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\vee \neg Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
55	23	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to X\in V$$
56		simprl	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to X\ne \underset{\dot{}}{0}$$
57		eldifsn	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in V\wedge X\ne \underset{\dot{}}{0}\right)$$
58	55 56 57	sylanbrc	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
59	24	adantr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to Y\in V$$
60		simprr	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to Y\ne \underset{\dot{}}{0}$$
61		eldifsn	$$⊢Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(Y\in V\wedge Y\ne \underset{\dot{}}{0}\right)$$
62	59 60 61	sylanbrc	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
63	1 2 3 4 5 6 7 8 9 10 11 12 13 14 47 48 49 50 51 52 53 54 58 62	lclkrlem2i	$$⊢\left(\phi \wedge \left(X\ne \underset{\dot{}}{0}\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)$$
64	35 46 63	pm2.61da2ne	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(E\underset{\dot{}}{+}G\right)\right)\right)=L\left(E\underset{\dot{}}{+}G\right)$$