Theorem mapdpglem18

Description: Lemma for mapdpg . Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	mapdpglem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	mapdpglem.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
	mapdpglem.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	mapdpglem.v	$$⊢V={\mathrm{Base}}_U$$
	mapdpglem.s	$$⊢\underset{\dot{}}{-}={-}_U$$
	mapdpglem.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	mapdpglem.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	mapdpglem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	mapdpglem.x	$$⊢\phi \to X\in V$$
	mapdpglem.y	$$⊢\phi \to Y\in V$$
	mapdpglem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(C\right)$$
	mapdpglem2.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
	mapdpglem3.f	$$⊢F={\mathrm{Base}}_C$$
	mapdpglem3.te	$$⊢\phi \to t\in \left(M\left(N\left(\left\{X\right\}\right)\right)\underset{\dot{}}{\oplus }M\left(N\left(\left\{Y\right\}\right)\right)\right)$$
	mapdpglem3.a	$$⊢A=\mathrm{Scalar}\left(U\right)$$
	mapdpglem3.b	$$⊢B={\mathrm{Base}}_A$$
	mapdpglem3.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	mapdpglem3.r	$$⊢R={-}_C$$
	mapdpglem3.g	$$⊢\phi \to G\in F$$
	mapdpglem3.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
	mapdpglem4.q	$$⊢Q=0_U$$
	mapdpglem.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	mapdpglem4.jt	$$⊢\phi \to M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{t\right\}\right)$$
	mapdpglem4.z	$$⊢\underset{\dot{}}{0}=0_A$$
	mapdpglem4.g4	$$⊢\phi \to g\in B$$
	mapdpglem4.z4	$$⊢\phi \to z\in M\left(N\left(\left\{Y\right\}\right)\right)$$
	mapdpglem4.t4	$$⊢\phi \to t=\left(g\underset{\dot{}}{·}G\right)Rz$$
	mapdpglem4.xn	$$⊢\phi \to X\ne Q$$
	mapdpglem12.yn	$$⊢\phi \to Y\ne Q$$
	mapdpglem17.ep	$$⊢E={inv}_r\left(A\right)\left(g\right)\underset{\dot{}}{·}z$$
Assertion	mapdpglem18	$$⊢\phi \to E\ne 0_C$$

Proof

Step	Hyp	Ref	Expression
1		mapdpglem.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		mapdpglem.m	$$⊢M=\mathrm{mapd}\left(K\right)\left(W\right)$$
3		mapdpglem.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		mapdpglem.v	$$⊢V={\mathrm{Base}}_U$$
5		mapdpglem.s	$$⊢\underset{\dot{}}{-}={-}_U$$
6		mapdpglem.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
7		mapdpglem.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		mapdpglem.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		mapdpglem.x	$$⊢\phi \to X\in V$$
10		mapdpglem.y	$$⊢\phi \to Y\in V$$
11		mapdpglem1.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(C\right)$$
12		mapdpglem2.j	$$⊢J=\mathrm{LSpan}\left(C\right)$$
13		mapdpglem3.f	$$⊢F={\mathrm{Base}}_C$$
14		mapdpglem3.te	$$⊢\phi \to t\in \left(M\left(N\left(\left\{X\right\}\right)\right)\underset{\dot{}}{\oplus }M\left(N\left(\left\{Y\right\}\right)\right)\right)$$
15		mapdpglem3.a	$$⊢A=\mathrm{Scalar}\left(U\right)$$
16		mapdpglem3.b	$$⊢B={\mathrm{Base}}_A$$
17		mapdpglem3.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
18		mapdpglem3.r	$$⊢R={-}_C$$
19		mapdpglem3.g	$$⊢\phi \to G\in F$$
20		mapdpglem3.e	$$⊢\phi \to M\left(N\left(\left\{X\right\}\right)\right)=J\left(\left\{G\right\}\right)$$
21		mapdpglem4.q	$$⊢Q=0_U$$
22		mapdpglem.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
23		mapdpglem4.jt	$$⊢\phi \to M\left(N\left(\left\{X\underset{\dot{}}{-}Y\right\}\right)\right)=J\left(\left\{t\right\}\right)$$
24		mapdpglem4.z	$$⊢\underset{\dot{}}{0}=0_A$$
25		mapdpglem4.g4	$$⊢\phi \to g\in B$$
26		mapdpglem4.z4	$$⊢\phi \to z\in M\left(N\left(\left\{Y\right\}\right)\right)$$
27		mapdpglem4.t4	$$⊢\phi \to t=\left(g\underset{\dot{}}{·}G\right)Rz$$
28		mapdpglem4.xn	$$⊢\phi \to X\ne Q$$
29		mapdpglem12.yn	$$⊢\phi \to Y\ne Q$$
30		mapdpglem17.ep	$$⊢E={inv}_r\left(A\right)\left(g\right)\underset{\dot{}}{·}z$$
31	1 3 8	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
32	15	lvecdrng	$$⊢U\in \mathrm{LVec}\to A\in \mathrm{DivRing}$$
33	31 32	syl	$$⊢\phi \to A\in \mathrm{DivRing}$$
34	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28	mapdpglem11	$$⊢\phi \to g\ne \underset{\dot{}}{0}$$
35		eqid	$$⊢{inv}_r\left(A\right)={inv}_r\left(A\right)$$
36	16 24 35	drnginvrn0	$$⊢\left(A\in \mathrm{DivRing}\wedge g\in B\wedge g\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(A\right)\left(g\right)\ne \underset{\dot{}}{0}$$
37	33 25 34 36	syl3anc	$$⊢\phi \to {inv}_r\left(A\right)\left(g\right)\ne \underset{\dot{}}{0}$$
38		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
39		eqid	$$⊢0_{\mathrm{Scalar}\left(C\right)}=0_{\mathrm{Scalar}\left(C\right)}$$
40	1 3 15 24 7 38 39 8	lcd0	$$⊢\phi \to 0_{\mathrm{Scalar}\left(C\right)}=\underset{\dot{}}{0}$$
41	37 40	neeqtrrd	$$⊢\phi \to {inv}_r\left(A\right)\left(g\right)\ne 0_{\mathrm{Scalar}\left(C\right)}$$
42	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29	mapdpglem16	$$⊢\phi \to z\ne 0_C$$
43		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
44		eqid	$$⊢0_C=0_C$$
45	1 7 8	lcdlvec	$$⊢\phi \to C\in \mathrm{LVec}$$
46	16 24 35	drnginvrcl	$$⊢\left(A\in \mathrm{DivRing}\wedge g\in B\wedge g\ne \underset{\dot{}}{0}\right)\to {inv}_r\left(A\right)\left(g\right)\in B$$
47	33 25 34 46	syl3anc	$$⊢\phi \to {inv}_r\left(A\right)\left(g\right)\in B$$
48	1 3 15 16 7 38 43 8	lcdsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}=B$$
49	47 48	eleqtrrd	$$⊢\phi \to {inv}_r\left(A\right)\left(g\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
50		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
51		eqid	$$⊢\mathrm{LSubSp}\left(C\right)=\mathrm{LSubSp}\left(C\right)$$
52	1 3 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
53	4 50 6	lspsncl	$$⊢\left(U\in \mathrm{LMod}\wedge Y\in V\right)\to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
54	52 10 53	syl2anc	$$⊢\phi \to N\left(\left\{Y\right\}\right)\in \mathrm{LSubSp}\left(U\right)$$
55	1 2 3 50 7 51 8 54	mapdcl2	$$⊢\phi \to M\left(N\left(\left\{Y\right\}\right)\right)\in \mathrm{LSubSp}\left(C\right)$$
56	13 51	lssss	$$⊢M\left(N\left(\left\{Y\right\}\right)\right)\in \mathrm{LSubSp}\left(C\right)\to M\left(N\left(\left\{Y\right\}\right)\right)\subseteq F$$
57	55 56	syl	$$⊢\phi \to M\left(N\left(\left\{Y\right\}\right)\right)\subseteq F$$
58	57 26	sseldd	$$⊢\phi \to z\in F$$
59	13 17 38 43 39 44 45 49 58	lvecvsn0	$$⊢\phi \to \left({inv}_r\left(A\right)\left(g\right)\underset{\dot{}}{·}z\ne 0_C\leftrightarrow \left({inv}_r\left(A\right)\left(g\right)\ne 0_{\mathrm{Scalar}\left(C\right)}\wedge z\ne 0_C\right)\right)$$
60	41 42 59	mpbir2and	$$⊢\phi \to {inv}_r\left(A\right)\left(g\right)\underset{\dot{}}{·}z\ne 0_C$$
61	60 30 44	3netr4g	$$⊢\phi \to E\ne 0_C$$