# Metamath Proof Explorer

## Theorem mapdh6jN

Description: Lemmma for mapdh6N . Eliminate ( N{ Y } ) = ( N{ Z } ) hypothesis. (Contributed by NM, 1-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdh.q ${⊢}{Q}={0}_{{C}}$
mapdh.i
mapdh.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdh.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdh.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdh.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdh.s
mapdhc.o
mapdh.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdh.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdh.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
mapdh.r ${⊢}{R}={-}_{{C}}$
mapdh.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdh.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdhc.f ${⊢}{\phi }\to {F}\in {D}$
mapdh.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
mapdhcl.x
mapdh.p
mapdh.a
mapdh6i.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
mapdh6i.y
mapdh6i.z
Assertion mapdh6jN

### Proof

Step Hyp Ref Expression
1 mapdh.q ${⊢}{Q}={0}_{{C}}$
2 mapdh.i
3 mapdh.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 mapdh.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
5 mapdh.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
6 mapdh.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
7 mapdh.s
8 mapdhc.o
9 mapdh.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
10 mapdh.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
11 mapdh.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
12 mapdh.r ${⊢}{R}={-}_{{C}}$
13 mapdh.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
14 mapdh.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
15 mapdhc.f ${⊢}{\phi }\to {F}\in {D}$
16 mapdh.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
17 mapdhcl.x
18 mapdh.p
19 mapdh.a
20 mapdh6i.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
21 mapdh6i.y
22 mapdh6i.z
23 14 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
24 15 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\right)\to {F}\in {D}$
25 16 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\right)\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
26 17 adantr
27 20 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\right)\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
28 21 adantr
29 22 adantr
30 simpr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)\right)\to {N}\left(\left\{{Y}\right\}\right)={N}\left(\left\{{Z}\right\}\right)$
31 1 2 3 4 5 6 7 8 9 10 11 12 13 23 24 25 26 18 19 27 28 29 30 mapdh6iN
32 14 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
33 15 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)\to {F}\in {D}$
34 16 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
35 17 adantr
36 21 adantr
37 22 adantr
38 20 adantr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
39 simpr ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
40 eqidd ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)\to {I}\left(⟨{X},{F},{Y}⟩\right)={I}\left(⟨{X},{F},{Y}⟩\right)$
41 eqidd ${⊢}\left({\phi }\wedge {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)\to {I}\left(⟨{X},{F},{Z}⟩\right)={I}\left(⟨{X},{F},{Z}⟩\right)$
42 1 2 3 4 5 6 7 8 9 10 11 12 13 32 33 34 35 18 19 36 37 38 39 40 41 mapdh6aN
43 31 42 pm2.61dane