Theorem lclkrlem2o

Description: Lemma for lclkr . When B is nonzero, the vectors X and Y can't both belong to the hyperplane generated by B . (Contributed by NM, 17-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)$$
	lclkrlem2o.b	$$⊢B=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)$$
	lclkrlem2o.n	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne \underset{\dot{}}{0}$$
	lclkrlem2o.bn	$$⊢\phi \to B\ne 0_U$$
Assertion	lclkrlem2o	$$⊢\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)$$

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		lclkrlem2o.b	$$⊢B=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)$$
23		lclkrlem2o.n	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne \underset{\dot{}}{0}$$
24		lclkrlem2o.bn	$$⊢\phi \to B\ne 0_U$$
25		eqid	$$⊢0_U=0_U$$
26	17 19 21	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
27	1 2 3 4 5 6 7 8 9 10 11 12 13 14 26 22 23	lclkrlem2m	$$⊢\phi \to \left(B\in V\wedge \left(E\underset{\dot{}}{+}G\right)\left(B\right)=\underset{\dot{}}{0}\right)$$
28	27	simpld	$$⊢\phi \to B\in V$$
29		eldifsn	$$⊢B\in \left(V\setminus \left\{0_U\right\}\right)\leftrightarrow \left(B\in V\wedge B\ne 0_U\right)$$
30	28 24 29	sylanbrc	$$⊢\phi \to B\in \left(V\setminus \left\{0_U\right\}\right)$$
31	17 18 19 1 25 21 30	dochnel	$$⊢\phi \to \neg B\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
32	17 19 21	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
33	32	adantr	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to U\in \mathrm{LMod}$$
34	28	snssd	$$⊢\phi \to \left\{B\right\}\subseteq V$$
35		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
36	17 19 1 35 18	dochlss	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge \left\{B\right\}\subseteq V\right)\to \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
37	21 34 36	syl2anc	$$⊢\phi \to \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
38	37	adantr	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
39		simprl	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
40	3	lmodring	$$⊢U\in \mathrm{LMod}\to S\in \mathrm{Ring}$$
41	32 40	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
42	8 9 10 32 13 14	ldualvaddcl	$$⊢\phi \to E\underset{\dot{}}{+}G\in F$$
43		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
44	3 43 1 8	lflcl	$$⊢\left(U\in \mathrm{LMod}\wedge E\underset{\dot{}}{+}G\in F\wedge X\in V\right)\to \left(E\underset{\dot{}}{+}G\right)\left(X\right)\in {\mathrm{Base}}_S$$
45	32 42 11 44	syl3anc	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(X\right)\in {\mathrm{Base}}_S$$
46	3	lvecdrng	$$⊢U\in \mathrm{LVec}\to S\in \mathrm{DivRing}$$
47	26 46	syl	$$⊢\phi \to S\in \mathrm{DivRing}$$
48	3 43 1 8	lflcl	$$⊢\left(U\in \mathrm{LMod}\wedge E\underset{\dot{}}{+}G\in F\wedge Y\in V\right)\to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\in {\mathrm{Base}}_S$$
49	32 42 12 48	syl3anc	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\in {\mathrm{Base}}_S$$
50	43 5 6	drnginvrcl	$$⊢\left(S\in \mathrm{DivRing}\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\in {\mathrm{Base}}_S\wedge \left(E\underset{\dot{}}{+}G\right)\left(Y\right)\ne \underset{\dot{}}{0}\right)\to I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\in {\mathrm{Base}}_S$$
51	47 49 23 50	syl3anc	$$⊢\phi \to I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\in {\mathrm{Base}}_S$$
52	43 4	ringcl	$$⊢\left(S\in \mathrm{Ring}\wedge \left(E\underset{\dot{}}{+}G\right)\left(X\right)\in {\mathrm{Base}}_S\wedge I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\in {\mathrm{Base}}_S\right)\to \left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\in {\mathrm{Base}}_S$$
53	41 45 51 52	syl3anc	$$⊢\phi \to \left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\in {\mathrm{Base}}_S$$
54	53	adantr	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to \left(E\underset{\dot{}}{+}G\right)\left(X\right)\underset{\dot{}}{\times }I\left(\left(E\underset{\dot{}}{+}G\right)\left(Y\right)\right)\in {\mathrm{Base}}_S$$
55		simprr	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
56	3 2 43 35	lssvscl	$$⊢\left(\left(U\in \mathrm{LMod}\wedge \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\in \mathrm{LSubSp}\left(U\right)\right)\wedge \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)\in {\mathrm{Base}}_S\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to \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\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
57	33 38 54 55 56	syl22anc	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to \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\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
58	7 35	lssvsubcl	$$⊢\left(\left(U\in \mathrm{LMod}\wedge \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\in \mathrm{LSubSp}\left(U\right)\right)\wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge \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\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\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)\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
59	33 38 39 57 58	syl22anc	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\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)\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
60	22 59	eqeltrid	$$⊢\left(\phi \wedge \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\right)\to B\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)$$
61	31 60	mtand	$$⊢\phi \to \neg \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)$$
62		ianor	$$⊢\neg \left(X\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\wedge Y\in \underset{\dot{}}{\perp }\left(\left\{B\right\}\right)\right)\leftrightarrow \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)$$
63	61 62	sylib	$$⊢\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)$$