# Metamath Proof Explorer

## Theorem hdmap1l6

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 . (Convert mapdh6N to use the function HDMap1 .) (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmap1-6.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmap1-6.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmap1-6.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmap1-6.p
hdmap1-6.o
hdmap1-6.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
hdmap1-6.c ${⊢}{C}=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
hdmap1-6.d ${⊢}{D}={\mathrm{Base}}_{{C}}$
hdmap1-6.a
hdmap1-6.l ${⊢}{L}=\mathrm{LSpan}\left({C}\right)$
hdmap1-6.m ${⊢}{M}=\mathrm{mapd}\left({K}\right)\left({W}\right)$
hdmap1-6.i ${⊢}{I}=\mathrm{HDMap1}\left({K}\right)\left({W}\right)$
hdmap1-6.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmap1-6.f ${⊢}{\phi }\to {F}\in {D}$
hdmap1-6.x
hdmap1-6.y ${⊢}{\phi }\to {Y}\in {V}$
hdmap1-6.z ${⊢}{\phi }\to {Z}\in {V}$
hdmap1-6.xn ${⊢}{\phi }\to ¬{X}\in {N}\left(\left\{{Y},{Z}\right\}\right)$
hdmap1-6.mn ${⊢}{\phi }\to {M}\left({N}\left(\left\{{X}\right\}\right)\right)={L}\left(\left\{{F}\right\}\right)$
Assertion hdmap1l6

### Proof

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