# Metamath Proof Explorer

## Theorem mapdpglem24

Description: Lemma for mapdpg . Existence part - consolidate hypotheses in mapdpglem23 . (Contributed by NM, 21-Mar-2015)

Ref Expression
Hypotheses mapdpg.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdpg.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdpg.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdpg.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdpg.s
mapdpg.z
mapdpg.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdpg.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdpg.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
mapdpg.r ${⊢}{R}={-}_{{C}}$
mapdpg.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdpg.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdpg.x
mapdpg.y
mapdpg.g ${⊢}{\phi }\to {G}\in {F}$
mapdpg.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
mapdpg.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
Assertion mapdpglem24

### Proof

Step Hyp Ref Expression
1 mapdpg.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdpg.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
3 mapdpg.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 mapdpg.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 mapdpg.s
6 mapdpg.z
7 mapdpg.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
8 mapdpg.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
9 mapdpg.f ${⊢}{F}={\mathrm{Base}}_{{C}}$
10 mapdpg.r ${⊢}{R}={-}_{{C}}$
11 mapdpg.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 mapdpg.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
13 mapdpg.x
14 mapdpg.y
15 mapdpg.g ${⊢}{\phi }\to {G}\in {F}$
16 mapdpg.ne ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
17 mapdpg.e ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
18 13 eldifad ${⊢}{\phi }\to {X}\in {V}$
19 14 eldifad ${⊢}{\phi }\to {Y}\in {V}$
20 eqid ${⊢}\mathrm{LSSum}\left({C}\right)=\mathrm{LSSum}\left({C}\right)$
21 1 2 3 4 5 7 8 12 18 19 20 11 mapdpglem2
25 simp2
26 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
27 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}$
28 eqid ${⊢}{\cdot }_{{C}}={\cdot }_{{C}}$
31 1 2 3 4 5 7 8 22 23 24 20 11 9 25 26 27 28 10 29 30 mapdpglem3
35 simp12
40 simp13
41 eqid ${⊢}{0}_{\mathrm{Scalar}\left({U}\right)}={0}_{\mathrm{Scalar}\left({U}\right)}$
42 simp2l
43 simp2r
44 simp3
45 eldifsni
46 13 45 syl
53 eqid ${⊢}{inv}_{r}\left(\mathrm{Scalar}\left({U}\right)\right)\left({g}\right){\cdot }_{{C}}{z}={inv}_{r}\left(\mathrm{Scalar}\left({U}\right)\right)\left({g}\right){\cdot }_{{C}}{z}$