# 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 = ( LHyp ` K )`
hdmap1-6.u
`|- U = ( ( DVecH ` K ) ` W )`
hdmap1-6.v
`|- V = ( Base ` U )`
hdmap1-6.p
`|- .+ = ( +g ` U )`
hdmap1-6.o
`|- .0. = ( 0g ` U )`
hdmap1-6.n
`|- N = ( LSpan ` U )`
hdmap1-6.c
`|- C = ( ( LCDual ` K ) ` W )`
hdmap1-6.d
`|- D = ( Base ` C )`
hdmap1-6.a
`|- .+b = ( +g ` C )`
hdmap1-6.l
`|- L = ( LSpan ` C )`
hdmap1-6.m
`|- M = ( ( mapd ` K ) ` W )`
hdmap1-6.i
`|- I = ( ( HDMap1 ` K ) ` W )`
hdmap1-6.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
hdmap1-6.f
`|- ( ph -> F e. D )`
hdmap1-6.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
hdmap1-6.y
`|- ( ph -> Y e. V )`
hdmap1-6.z
`|- ( ph -> Z e. V )`
hdmap1-6.xn
`|- ( ph -> -. X e. ( N ` { Y , Z } ) )`
hdmap1-6.mn
`|- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )`
Assertion hdmap1l6
`|- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )`

### Proof

Step Hyp Ref Expression
1 hdmap1-6.h
` |-  H = ( LHyp ` K )`
2 hdmap1-6.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 hdmap1-6.v
` |-  V = ( Base ` U )`
4 hdmap1-6.p
` |-  .+ = ( +g ` U )`
5 hdmap1-6.o
` |-  .0. = ( 0g ` U )`
6 hdmap1-6.n
` |-  N = ( LSpan ` U )`
7 hdmap1-6.c
` |-  C = ( ( LCDual ` K ) ` W )`
8 hdmap1-6.d
` |-  D = ( Base ` C )`
9 hdmap1-6.a
` |-  .+b = ( +g ` C )`
10 hdmap1-6.l
` |-  L = ( LSpan ` C )`
11 hdmap1-6.m
` |-  M = ( ( mapd ` K ) ` W )`
12 hdmap1-6.i
` |-  I = ( ( HDMap1 ` K ) ` W )`
13 hdmap1-6.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
14 hdmap1-6.f
` |-  ( ph -> F e. D )`
15 hdmap1-6.x
` |-  ( ph -> X e. ( V \ { .0. } ) )`
16 hdmap1-6.y
` |-  ( ph -> Y e. V )`
17 hdmap1-6.z
` |-  ( ph -> Z e. V )`
18 hdmap1-6.xn
` |-  ( ph -> -. X e. ( N ` { Y , Z } ) )`
19 hdmap1-6.mn
` |-  ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )`
20 eqid
` |-  ( -g ` U ) = ( -g ` U )`
21 eqid
` |-  ( -g ` C ) = ( -g ` C )`
22 eqid
` |-  ( 0g ` C ) = ( 0g ` 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
` |-  ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )`