Metamath Proof Explorer

Theorem mapdpglem17N

Description: Lemma for mapdpg . Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015) (New usage is discouraged.)

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 mapdpglem17N ${⊢}{\phi }\to {E}\in {F}$

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 drnginvrcl
37 33 25 34 36 syl3anc ${⊢}{\phi }\to {inv}_{r}\left({A}\right)\left({g}\right)\in {B}$
38 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
39 eqid ${⊢}\mathrm{LSubSp}\left({C}\right)=\mathrm{LSubSp}\left({C}\right)$
40 1 3 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
41 4 38 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)$
42 40 10 41 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
43 1 2 3 38 7 39 8 42 mapdcl2 ${⊢}{\phi }\to {M}\left({N}\left(\left\{{Y}\right\}\right)\right)\in \mathrm{LSubSp}\left({C}\right)$
44 13 39 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}$
45 43 44 syl ${⊢}{\phi }\to {M}\left({N}\left(\left\{{Y}\right\}\right)\right)\subseteq {F}$
46 45 26 sseldd ${⊢}{\phi }\to {z}\in {F}$
47 1 3 15 16 7 13 17 8 37 46 lcdvscl
48 30 47 eqeltrid ${⊢}{\phi }\to {E}\in {F}$