# Metamath Proof Explorer

## Theorem mapdh8ab

Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 13-May-2015)

Ref Expression
Hypotheses mapdh8a.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
mapdh8a.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
mapdh8a.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
mapdh8a.s
mapdh8a.o
mapdh8a.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
mapdh8a.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
mapdh8a.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
mapdh8a.r ${⊢}{R}={-}_{{C}}$
mapdh8a.q ${⊢}{Q}={0}_{{C}}$
mapdh8a.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
mapdh8a.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
mapdh8a.i
mapdh8a.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
mapdh8ab.f ${⊢}{\phi }\to {F}\in {D}$
mapdh8ab.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
mapdh8ab.eg ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
mapdh8ab.ee ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)={E}$
mapdh8ab.x
mapdh8ab.y
mapdh8ab.z
mapdh8ab.t
mapdh8ab.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
mapdh8ab.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
mapdh8ab.yn ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{T}\right\}\right)$
Assertion mapdh8ab ${⊢}{\phi }\to {I}\left(⟨{Y},{G},{T}⟩\right)={I}\left(⟨{Z},{E},{T}⟩\right)$

### Proof

Step Hyp Ref Expression
1 mapdh8a.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdh8a.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 mapdh8a.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 mapdh8a.s
5 mapdh8a.o
6 mapdh8a.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
7 mapdh8a.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
8 mapdh8a.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
9 mapdh8a.r ${⊢}{R}={-}_{{C}}$
10 mapdh8a.q ${⊢}{Q}={0}_{{C}}$
11 mapdh8a.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
12 mapdh8a.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
13 mapdh8a.i
14 mapdh8a.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
15 mapdh8ab.f ${⊢}{\phi }\to {F}\in {D}$
16 mapdh8ab.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
17 mapdh8ab.eg ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
18 mapdh8ab.ee ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)={E}$
19 mapdh8ab.x
20 mapdh8ab.y
21 mapdh8ab.z
22 mapdh8ab.t
23 mapdh8ab.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
24 mapdh8ab.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
25 mapdh8ab.yn ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)={N}\left(\left\{{T}\right\}\right)$
26 1 2 14 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
27 19 eldifad ${⊢}{\phi }\to {X}\in {V}$
28 20 eldifad ${⊢}{\phi }\to {Y}\in {V}$
29 21 eldifad ${⊢}{\phi }\to {Z}\in {V}$
30 3 6 26 27 28 29 24 lspindpi ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\right)$
31 30 simprd ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
32 31 necomd ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\ne {N}\left(\left\{{X}\right\}\right)$
33 32 25 neeqtrd ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\ne {N}\left(\left\{{T}\right\}\right)$
34 25 sseq1d ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)↔{N}\left(\left\{{T}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
35 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
36 1 2 14 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
37 3 35 6 36 28 29 lspprcl ${⊢}{\phi }\to {N}\left(\left\{{Y},{Z}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
38 3 35 6 36 37 27 lspsnel5 ${⊢}{\phi }\to \left({X}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔{N}\left(\left\{{X}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
39 22 eldifad ${⊢}{\phi }\to {T}\in {V}$
40 3 35 6 36 37 39 lspsnel5 ${⊢}{\phi }\to \left({T}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔{N}\left(\left\{{T}\right\}\right)\subseteq {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
41 34 38 40 3bitr4d ${⊢}{\phi }\to \left({X}\in {N}\left(\left\{{Y},{Z}\right\}\right)↔{T}\in {N}\left(\left\{{Y},{Z}\right\}\right)\right)$
42 24 41 mtbid ${⊢}{\phi }\to ¬{T}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
43 26 adantr ${⊢}\left({\phi }\wedge {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)\right)\to {U}\in \mathrm{LVec}$
45 39 adantr ${⊢}\left({\phi }\wedge {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)\right)\to {T}\in {V}$
46 29 adantr ${⊢}\left({\phi }\wedge {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)\right)\to {Z}\in {V}$
47 23 adantr ${⊢}\left({\phi }\wedge {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)\right)\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
48 simpr ${⊢}\left({\phi }\wedge {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)\right)\to {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)$
49 prcom ${⊢}\left\{{Z},{T}\right\}=\left\{{T},{Z}\right\}$
50 49 fveq2i ${⊢}{N}\left(\left\{{Z},{T}\right\}\right)={N}\left(\left\{{T},{Z}\right\}\right)$
51 48 50 eleqtrdi ${⊢}\left({\phi }\wedge {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)\right)\to {Y}\in {N}\left(\left\{{T},{Z}\right\}\right)$
52 3 5 6 43 44 45 46 47 51 lspexch ${⊢}\left({\phi }\wedge {Y}\in {N}\left(\left\{{Z},{T}\right\}\right)\right)\to {T}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
53 42 52 mtand ${⊢}{\phi }\to ¬{Y}\in {N}\left(\left\{{Z},{T}\right\}\right)$
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 33 22 53 24 mapdh8aa ${⊢}{\phi }\to {I}\left(⟨{Y},{G},{T}⟩\right)={I}\left(⟨{Z},{E},{T}⟩\right)$