Theorem lclkrlem2x

Description: Lemma for lclkr . Eliminate by cases the hypotheses of lclkrlem2u , lclkrlem2u and lclkrlem2w . (Contributed by NM, 18-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2x.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lclkrlem2x.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lclkrlem2x.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lclkrlem2x.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lclkrlem2x.v	$$⊢V={\mathrm{Base}}_U$$
	lclkrlem2x.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lclkrlem2x.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lclkrlem2x.p	$$⊢\underset{\dot{}}{+}={+}_D$$
	lclkrlem2x.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lclkrlem2x.x	$$⊢\phi \to X\in V$$
	lclkrlem2x.y	$$⊢\phi \to Y\in V$$
	lclkrlem2x.e	$$⊢\phi \to E\in F$$
	lclkrlem2x.g	$$⊢\phi \to G\in F$$
	lclkrlem2x.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
	lclkrlem2x.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
Assertion	lclkrlem2x	$$⊢\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		lclkrlem2x.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
2		lclkrlem2x.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
3		lclkrlem2x.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
4		lclkrlem2x.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		lclkrlem2x.v	$$⊢V={\mathrm{Base}}_U$$
6		lclkrlem2x.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		lclkrlem2x.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		lclkrlem2x.p	$$⊢\underset{\dot{}}{+}={+}_D$$
9		lclkrlem2x.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lclkrlem2x.x	$$⊢\phi \to X\in V$$
11		lclkrlem2x.y	$$⊢\phi \to Y\in V$$
12		lclkrlem2x.e	$$⊢\phi \to E\in F$$
13		lclkrlem2x.g	$$⊢\phi \to G\in F$$
14		lclkrlem2x.le	$$⊢\phi \to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
15		lclkrlem2x.lg	$$⊢\phi \to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
16		df-ne	$$⊢\left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\leftrightarrow \neg \left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}$$
17		eqid	$$⊢{\cdot }_U={\cdot }_U$$
18		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
19		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(U\right)}={\cdot }_{\mathrm{Scalar}\left(U\right)}$$
20		eqid	$$⊢0_{\mathrm{Scalar}\left(U\right)}=0_{\mathrm{Scalar}\left(U\right)}$$
21		eqid	$$⊢{inv}_r\left(\mathrm{Scalar}\left(U\right)\right)={inv}_r\left(\mathrm{Scalar}\left(U\right)\right)$$
22		eqid	$$⊢{-}_U={-}_U$$
23	10	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to X\in V$$
24	11	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to Y\in V$$
25	12	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to E\in F$$
26	13	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to G\in F$$
27		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
28		eqid	$$⊢\mathrm{LSSum}\left(U\right)=\mathrm{LSSum}\left(U\right)$$
29	9	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
30	14	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
31	15	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
32		simpr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\right)}$$
33	5 17 18 19 20 21 22 6 7 8 23 24 25 26 27 1 2 3 4 28 29 30 31 32	lclkrlem2u	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\ne 0_{\mathrm{Scalar}\left(U\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)$$
34	16 33	sylan2br	$$⊢\left(\phi \wedge \neg \left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\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)$$
35		df-ne	$$⊢\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\leftrightarrow \neg \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}$$
36	10	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to X\in V$$
37	11	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to Y\in V$$
38	12	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to E\in F$$
39	13	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to G\in F$$
40	9	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
41	14	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
42	15	adantr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
43		simpr	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}\right)\to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\right)}$$
44	5 17 18 19 20 21 22 6 7 8 36 37 38 39 27 1 2 3 4 28 40 41 42 43	lclkrlem2t	$$⊢\left(\phi \wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne 0_{\mathrm{Scalar}\left(U\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)$$
45	35 44	sylan2br	$$⊢\left(\phi \wedge \neg \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\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)$$
46	10	adantr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to X\in V$$
47	11	adantr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to Y\in V$$
48	12	adantr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to E\in F$$
49	13	adantr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to G\in F$$
50	9	adantr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
51	14	adantr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to L\left(E\right)=\underset{\dot{}}{\perp }\left(\left\{X\right\}\right)$$
52	15	adantr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to L\left(G\right)=\underset{\dot{}}{\perp }\left(\left\{Y\right\}\right)$$
53		simprl	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to \left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}$$
54		simprr	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\right)\right)\to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}$$
55	5 17 18 19 20 21 22 6 7 8 46 47 48 49 27 1 2 3 4 28 50 51 52 53 54	lclkrlem2w	$$⊢\left(\phi \wedge \left(\left(E\underset{\dot{}}{+}G\right)\left(X\right)=0_{\mathrm{Scalar}\left(U\right)}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)=0_{\mathrm{Scalar}\left(U\right)}\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)$$
56	34 45 55	pm2.61dda	$$⊢\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)$$