Theorem lclkrlem2t

Description: Lemma for lclkr . We eliminate all hypotheses with B here. (Contributed by NM, 18-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	$$⊢V={\mathrm{Base}}_U$$
	lclkrlem2m.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lclkrlem2m.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lclkrlem2m.q	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
	lclkrlem2m.z	$$⊢\underset{\dot{}}{0}=0_S$$
	lclkrlem2m.i	$$⊢I={inv}_r\left(S\right)$$
	lclkrlem2m.m	$$⊢\underset{\dot{}}{-}={-}_U$$
	lclkrlem2m.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lclkrlem2m.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lclkrlem2m.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	lclkrlem2m.x	$$⊢\phi \to X\in V$$
	lclkrlem2m.y	$$⊢\phi \to Y\in V$$
	lclkrlem2m.e	$$⊢\phi \to E\in F$$
	lclkrlem2m.g	$$⊢\phi \to G\in F$$
	lclkrlem2n.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lclkrlem2n.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lclkrlem2o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lclkrlem2o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lclkrlem2o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lclkrlem2o.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
	lclkrlem2o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lclkrlem2q.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
	lclkrlem2q.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
	lclkrlem2t.n	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne \underset{\dot{}}{0}$$
Assertion	lclkrlem2t	$$⊢\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		lclkrlem2m.v	$$⊢V={\mathrm{Base}}_U$$
2		lclkrlem2m.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
3		lclkrlem2m.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
4		lclkrlem2m.q	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
5		lclkrlem2m.z	$$⊢\underset{\dot{}}{0}=0_S$$
6		lclkrlem2m.i	$$⊢I={inv}_r\left(S\right)$$
7		lclkrlem2m.m	$$⊢\underset{\dot{}}{-}={-}_U$$
8		lclkrlem2m.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
9		lclkrlem2m.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
10		lclkrlem2m.p	$$⊢\underset{\dot{}}{+}={+}_D$$
11		lclkrlem2m.x	$$⊢\phi \to X\in V$$
12		lclkrlem2m.y	$$⊢\phi \to Y\in V$$
13		lclkrlem2m.e	$$⊢\phi \to E\in F$$
14		lclkrlem2m.g	$$⊢\phi \to G\in F$$
15		lclkrlem2n.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
16		lclkrlem2n.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
17		lclkrlem2o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
18		lclkrlem2o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
19		lclkrlem2o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
20		lclkrlem2o.a	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(U\right)$$
21		lclkrlem2o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
22		lclkrlem2q.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
23		lclkrlem2q.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
24		lclkrlem2t.n	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne \underset{\dot{}}{0}$$
25	11	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to X\in V$$
26	12	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to Y\in V$$
27	13	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to E\in F$$
28	14	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to G\in F$$
29	21	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
30	22	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
31	23	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
32		eqid	$$⊢X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)$$
33	24	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne \underset{\dot{}}{0}$$
34		simpr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\right)\to X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U$$
35	1 2 3 4 5 6 7 8 9 10 25 26 27 28 15 16 17 18 19 20 29 30 31 32 33 34	lclkrlem2s	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)=0_U\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	11	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to X\in V$$
37	12	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to Y\in V$$
38	13	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to E\in F$$
39	14	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to G\in F$$
40	21	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
41	22	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
42	23	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
43	24	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne \underset{\dot{}}{0}$$
44		simpr	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\right)\to X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U$$
45	1 2 3 4 5 6 7 8 9 10 36 37 38 39 15 16 17 18 19 20 40 41 42 32 43 44	lclkrlem2q	$$⊢\left(\phi \wedge X\underset{\dot{}}{-}\left(\left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\right)\underset{\dot{}}{·}Y\right)\ne 0_U\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)$$
46	35 45	pm2.61dane	$$⊢\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)$$