# Metamath Proof Explorer

## Theorem mapdh6N

Description: Part (6) of Baer p. 47 line 6. Note that we use -. X e. ( N{ Y , Z } ) which is equivalent to Baer's "Fx i^i (Fy + Fz)" by lspdisjb . TODO: If disjoint variable conditions with I and ph become a problem later, use cbv* theorems on I variables here to get rid of them. Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. TODO: may be deleted (with its lemmas), if not needed, in view of hdmap1l6 . (Contributed by NM, 1-May-2015) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 mapdh6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 mapdh6.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 mapdh6.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 mapdh6.p
5 mapdh6.s
6 mapdh6.o
7 mapdh6.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
8 mapdh6.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
9 mapdh6.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
10 mapdh6.a
11 mapdh6.r ${⊢}{R}={-}_{{C}}$
12 mapdh6.q ${⊢}{Q}={0}_{{C}}$
13 mapdh6.j ${⊢}{J}=\mathrm{LSpan}\left({C}\right)$
14 mapdh6.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
15 mapdh6.i
16 mapdh6.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
17 mapdh6.f ${⊢}{\phi }\to {F}\in {D}$
18 mapdh6.x
19 mapdh6.y ${⊢}{\phi }\to {Y}\in {V}$
20 mapdh6.z ${⊢}{\phi }\to {Z}\in {V}$
21 mapdh6.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
22 mapdh6.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={J}\left(\left\{{F}\right\}\right)$
23 12 15 1 14 2 3 5 6 7 8 9 11 13 16 17 22 18 4 10 19 20 21 mapdh6kN