# Metamath Proof Explorer

## Theorem mapdh6lem1N

Description: Lemma for mapdh6N . Part (6) in Baer p. 47, lines 16-18. (Contributed by NM, 13-Apr-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
mapdhe6.y
mapdhe6.z
mapdhe6.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
mapdh6.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
mapdh6.fg ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
mapdh6.fe ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)={E}$
Assertion mapdh6lem1N

### 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 mapdhe6.y
21 mapdhe6.z
22 mapdhe6.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
23 mapdh6.yz ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
24 mapdh6.fg ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)={G}$
25 mapdh6.fe ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)={E}$
26 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
27 3 5 14 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
28 17 eldifad ${⊢}{\phi }\to {X}\in {V}$
29 20 eldifad ${⊢}{\phi }\to {Y}\in {V}$
30 6 7 lmodvsubcl
31 27 28 29 30 syl3anc
32 6 26 9 lspsncl
33 27 31 32 syl2anc
34 21 eldifad ${⊢}{\phi }\to {Z}\in {V}$
35 6 26 9 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {Z}\in {V}\right)\to {N}\left(\left\{{Z}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
36 27 34 35 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Z}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
37 eqid ${⊢}\mathrm{LSSum}\left({U}\right)=\mathrm{LSSum}\left({U}\right)$
38 26 37 lsmcl
39 27 33 36 38 syl3anc
40 6 7 lmodvsubcl
41 27 28 34 40 syl3anc
42 6 26 9 lspsncl
43 27 41 42 syl2anc
44 6 26 9 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {Y}\in {V}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
45 27 29 44 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
46 26 37 lsmcl
47 27 43 45 46 syl3anc
48 3 4 5 26 14 39 47 mapdin
49 eqid ${⊢}\mathrm{LSSum}\left({C}\right)=\mathrm{LSSum}\left({C}\right)$
50 3 4 5 26 37 10 49 14 33 36 mapdlsm
51 3 4 5 26 37 10 49 14 43 45 mapdlsm
52 50 51 ineq12d
53 3 5 14 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
54 6 8 9 53 29 21 28 23 22 lspindp2 ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)\wedge ¬{Z}\in {N}\left(\left\{{X},{Y}\right\}\right)\right)$
55 54 simpld ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Y}\right\}\right)$
56 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 29 55 mapdhcl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Y}⟩\right)\in {D}$
57 24 56 eqeltrrd ${⊢}{\phi }\to {G}\in {D}$
58 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 20 57 55 mapdheq
59 24 58 mpbid
60 59 simprd
61 6 8 9 53 20 34 28 23 22 lspindp1 ${⊢}{\phi }\to \left({N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)\wedge ¬{Y}\in {N}\left(\left\{{X},{Z}\right\}\right)\right)$
62 61 simpld ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\ne {N}\left(\left\{{Z}\right\}\right)$
63 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 34 62 mapdhcl ${⊢}{\phi }\to {I}\left(⟨{X},{F},{Z}⟩\right)\in {D}$
64 25 63 eqeltrrd ${⊢}{\phi }\to {E}\in {D}$
65 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 21 64 62 mapdheq
66 25 65 mpbid
67 66 simpld ${⊢}{\phi }\to {M}\left({N}\left(\left\{{Z}\right\}\right)\right)={J}\left(\left\{{E}\right\}\right)$
68 60 67 oveq12d
69 66 simprd
70 59 simpld ${⊢}{\phi }\to {M}\left({N}\left(\left\{{Y}\right\}\right)\right)={J}\left(\left\{{G}\right\}\right)$
71 69 70 oveq12d
72 68 71 ineq12d
73 52 72 eqtrd
74 48 73 eqtrd
75 6 7 8 37 9 53 28 22 23 20 21 18 baerlem5a
76 75 fveq2d
77 3 10 14 lcdlvec ${⊢}{\phi }\to {C}\in \mathrm{LVec}$
78 3 4 5 6 9 10 11 13 14 15 16 28 29 57 70 34 64 67 22 mapdindp ${⊢}{\phi }\to ¬{F}\in {J}\left(\left\{{G},{E}\right\}\right)$
79 3 4 5 6 9 10 11 13 14 57 70 29 34 64 67 23 mapdncol ${⊢}{\phi }\to {J}\left(\left\{{G}\right\}\right)\ne {J}\left(\left\{{E}\right\}\right)$
80 3 4 5 6 9 10 11 13 14 57 70 8 1 20 mapdn0 ${⊢}{\phi }\to {G}\in \left({D}\setminus \left\{{Q}\right\}\right)$
81 3 4 5 6 9 10 11 13 14 64 67 8 1 21 mapdn0 ${⊢}{\phi }\to {E}\in \left({D}\setminus \left\{{Q}\right\}\right)$
82 11 12 1 49 13 77 15 78 79 80 81 19 baerlem5a
83 74 76 82 3eqtr4d