# Metamath Proof Explorer

## Theorem hdmap1eulem

Description: Lemma for hdmap1eu . TODO: combine with hdmap1eu or at least share some hypotheses. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmap1eulem.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmap1eulem.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmap1eulem.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmap1eulem.s
hdmap1eulem.o
hdmap1eulem.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmap1eulem.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmap1eulem.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmap1eulem.r ${⊢}{R}={-}_{{C}}$
hdmap1eulem.q ${⊢}{Q}={0}_{{C}}$
hdmap1eulem.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
hdmap1eulem.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
hdmap1eulem.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmap1eulem.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmap1eulem.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
hdmap1eulem.x
hdmap1eulem.f ${⊢}{\phi }\to {F}\in {D}$
hdmap1eulem.y ${⊢}{\phi }\to {T}\in {V}$
hdmap1eulem.l
Assertion hdmap1eulem ${⊢}{\phi }\to \exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)$

### Proof

Step Hyp Ref Expression
1 hdmap1eulem.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmap1eulem.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hdmap1eulem.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 hdmap1eulem.s
5 hdmap1eulem.o
6 hdmap1eulem.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
7 hdmap1eulem.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
8 hdmap1eulem.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
9 hdmap1eulem.r ${⊢}{R}={-}_{{C}}$
10 hdmap1eulem.q ${⊢}{Q}={0}_{{C}}$
11 hdmap1eulem.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 hdmap1eulem.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
13 hdmap1eulem.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
14 hdmap1eulem.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
15 hdmap1eulem.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
16 hdmap1eulem.x
17 hdmap1eulem.f ${⊢}{\phi }\to {F}\in {D}$
18 hdmap1eulem.y ${⊢}{\phi }\to {T}\in {V}$
19 hdmap1eulem.l
20 1 2 3 4 5 6 7 8 9 10 11 12 19 14 17 15 16 18 mapdh9a ${⊢}{\phi }\to \exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)$
21 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
23 17 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to {F}\in {D}$
24 simplr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to {z}\in {V}$
25 1 2 3 4 5 6 7 8 9 10 11 12 13 21 22 23 24 19 hdmap1valc ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to {I}\left(⟨{X},{F},{z}⟩\right)={L}\left(⟨{X},{F},{z}⟩\right)$
26 25 oteq2d ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to ⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩=⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩$
27 26 fveq2d ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to {I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)={I}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)$
28 elun1 ${⊢}{z}\in {N}\left(\left\{{X}\right\}\right)\to {z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)$
29 28 con3i ${⊢}¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to ¬{z}\in {N}\left(\left\{{X}\right\}\right)$
30 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
31 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
32 1 2 14 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
33 32 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {U}\in \mathrm{LMod}$
34 16 eldifad ${⊢}{\phi }\to {X}\in {V}$
35 34 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {X}\in {V}$
36 3 31 6 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
37 33 35 36 syl2anc ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
38 simplr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {z}\in {V}$
39 simpr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to ¬{z}\in {N}\left(\left\{{X}\right\}\right)$
40 5 31 33 37 38 39 lssneln0
41 17 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {F}\in {D}$
42 15 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
44 3 6 33 38 35 39 lspsnne2 ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {N}\left(\left\{{z}\right\}\right)\ne {N}\left(\left\{{X}\right\}\right)$
45 44 necomd ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{z}\right\}\right)$
46 10 19 1 12 2 3 4 5 6 7 8 9 11 30 41 42 43 38 45 mapdhcl ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {L}\left(⟨{X},{F},{z}⟩\right)\in {D}$
47 18 ad2antrr ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {T}\in {V}$
48 1 2 3 4 5 6 7 8 9 10 11 12 13 30 40 46 47 19 hdmap1valc ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in {N}\left(\left\{{X}\right\}\right)\right)\to {I}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)$
49 29 48 sylan2 ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to {I}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)$
50 27 49 eqtrd ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to {I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)$
51 50 eqeq2d ${⊢}\left(\left({\phi }\wedge {z}\in {V}\right)\wedge ¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\right)\to \left({y}={I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)↔{y}={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)$
52 51 pm5.74da ${⊢}\left({\phi }\wedge {z}\in {V}\right)\to \left(\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)↔\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)\right)$
53 52 ralbidva ${⊢}{\phi }\to \left(\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)↔\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)\right)$
54 53 reubidv ${⊢}{\phi }\to \left(\exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)↔\exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={L}\left(⟨{z},{L}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)\right)$
55 20 54 mpbird ${⊢}{\phi }\to \exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}\forall {z}\in {V}\phantom{\rule{.4em}{0ex}}\left(¬{z}\in \left({N}\left(\left\{{X}\right\}\right)\cup {N}\left(\left\{{T}\right\}\right)\right)\to {y}={I}\left(⟨{z},{I}\left(⟨{X},{F},{z}⟩\right),{T}⟩\right)\right)$