# Metamath Proof Explorer

## 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
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
mapdpglem2.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdpglem3.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
mapdpglem3.te
mapdpglem3.a ${⊢}{A}=\mathrm{Scalar}\left({U}\right)$
mapdpglem3.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
mapdpglem3.t
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
mapdpglem4.z
mapdpglem4.g4 ${⊢}{\phi }\to {g}\in {B}$
mapdpglem4.z4 ${⊢}{\phi }\to {z}\in {M}\left({N}\left(\left\{{Y}\right\}\right)\right)$
mapdpglem4.t4
mapdpglem4.xn ${⊢}{\phi }\to {X}\ne {Q}$
mapdpglem12.yn ${⊢}{\phi }\to {Y}\ne {Q}$
mapdpglem17.ep
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
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
12 mapdpglem2.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
13 mapdpglem3.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
14 mapdpglem3.te
15 mapdpglem3.a ${⊢}{A}=\mathrm{Scalar}\left({U}\right)$
16 mapdpglem3.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
17 mapdpglem3.t
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
24 mapdpglem4.z
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
28 mapdpglem4.xn ${⊢}{\phi }\to {X}\ne {Q}$
29 mapdpglem12.yn ${⊢}{\phi }\to {Y}\ne {Q}$
30 mapdpglem17.ep
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
35 eqid ${⊢}{inv}_{r}\left({A}\right)={inv}_{r}\left({A}\right)$
36 16 24 35 drnginvrn0
37 33 25 34 36 syl3anc
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
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
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
60 41 42 59 mpbir2and
61 60 30 44 3netr4g ${⊢}{\phi }\to {E}\ne {0}_{{C}}$