# Metamath Proof Explorer

## Theorem mapdpglem6

Description: Lemma for mapdpg . Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-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}$
mapdpglem4.g0
Assertion mapdpglem6 ${⊢}{\phi }\to {t}\in {M}\left({N}\left(\left\{{Y}\right\}\right)\right)$

### 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 mapdpglem4.g0
30 1 7 8 lcdlmod ${⊢}{\phi }\to {C}\in \mathrm{LMod}$
31 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
32 eqid ${⊢}\mathrm{LSubSp}\left({C}\right)=\mathrm{LSubSp}\left({C}\right)$
33 1 3 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
34 4 31 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)$
35 33 10 34 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
36 1 2 3 31 7 32 8 35 mapdcl2 ${⊢}{\phi }\to {M}\left({N}\left(\left\{{Y}\right\}\right)\right)\in \mathrm{LSubSp}\left({C}\right)$
37 29 oveq1d
38 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
39 1 3 15 24 7 13 17 38 8 19 lcd0vs
40 37 39 eqtrd
41 38 32 lss0cl ${⊢}\left({C}\in \mathrm{LMod}\wedge {M}\left({N}\left(\left\{{Y}\right\}\right)\right)\in \mathrm{LSubSp}\left({C}\right)\right)\to {0}_{{C}}\in {M}\left({N}\left(\left\{{Y}\right\}\right)\right)$
42 30 36 41 syl2anc ${⊢}{\phi }\to {0}_{{C}}\in {M}\left({N}\left(\left\{{Y}\right\}\right)\right)$
43 40 42 eqeltrd
44 18 32 lssvsubcl
45 30 36 43 26 44 syl22anc
46 27 45 eqeltrd ${⊢}{\phi }\to {t}\in {M}\left({N}\left(\left\{{Y}\right\}\right)\right)$