# Metamath Proof Explorer

## Theorem hdmap1l6f

Description: Lemmma for hdmap1l6 . Part (6) in Baer p. 47 line 38. (Contributed by NM, 1-May-2015)

Ref Expression
Hypotheses hdmap1l6.h
`|- H = ( LHyp ` K )`
hdmap1l6.u
`|- U = ( ( DVecH ` K ) ` W )`
hdmap1l6.v
`|- V = ( Base ` U )`
hdmap1l6.p
`|- .+ = ( +g ` U )`
hdmap1l6.s
`|- .- = ( -g ` U )`
hdmap1l6c.o
`|- .0. = ( 0g ` U )`
hdmap1l6.n
`|- N = ( LSpan ` U )`
hdmap1l6.c
`|- C = ( ( LCDual ` K ) ` W )`
hdmap1l6.d
`|- D = ( Base ` C )`
hdmap1l6.a
`|- .+b = ( +g ` C )`
hdmap1l6.r
`|- R = ( -g ` C )`
hdmap1l6.q
`|- Q = ( 0g ` C )`
hdmap1l6.l
`|- L = ( LSpan ` C )`
hdmap1l6.m
`|- M = ( ( mapd ` K ) ` W )`
hdmap1l6.i
`|- I = ( ( HDMap1 ` K ) ` W )`
hdmap1l6.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
hdmap1l6.f
`|- ( ph -> F e. D )`
hdmap1l6cl.x
`|- ( ph -> X e. ( V \ { .0. } ) )`
hdmap1l6.mn
`|- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )`
hdmap1l6d.xn
`|- ( ph -> -. X e. ( N ` { Y , Z } ) )`
hdmap1l6d.yz
`|- ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )`
hdmap1l6d.y
`|- ( ph -> Y e. ( V \ { .0. } ) )`
hdmap1l6d.z
`|- ( ph -> Z e. ( V \ { .0. } ) )`
hdmap1l6d.w
`|- ( ph -> w e. ( V \ { .0. } ) )`
hdmap1l6d.wn
`|- ( ph -> -. w e. ( N ` { X , Y } ) )`
Assertion hdmap1l6f
`|- ( ph -> ( I ` <. X , F , ( w .+ Y ) >. ) = ( ( I ` <. X , F , w >. ) .+b ( I ` <. X , F , Y >. ) ) )`

### Proof

Step Hyp Ref Expression
1 hdmap1l6.h
` |-  H = ( LHyp ` K )`
2 hdmap1l6.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 hdmap1l6.v
` |-  V = ( Base ` U )`
4 hdmap1l6.p
` |-  .+ = ( +g ` U )`
5 hdmap1l6.s
` |-  .- = ( -g ` U )`
6 hdmap1l6c.o
` |-  .0. = ( 0g ` U )`
7 hdmap1l6.n
` |-  N = ( LSpan ` U )`
8 hdmap1l6.c
` |-  C = ( ( LCDual ` K ) ` W )`
9 hdmap1l6.d
` |-  D = ( Base ` C )`
10 hdmap1l6.a
` |-  .+b = ( +g ` C )`
11 hdmap1l6.r
` |-  R = ( -g ` C )`
12 hdmap1l6.q
` |-  Q = ( 0g ` C )`
13 hdmap1l6.l
` |-  L = ( LSpan ` C )`
14 hdmap1l6.m
` |-  M = ( ( mapd ` K ) ` W )`
15 hdmap1l6.i
` |-  I = ( ( HDMap1 ` K ) ` W )`
16 hdmap1l6.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
17 hdmap1l6.f
` |-  ( ph -> F e. D )`
18 hdmap1l6cl.x
` |-  ( ph -> X e. ( V \ { .0. } ) )`
19 hdmap1l6.mn
` |-  ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )`
20 hdmap1l6d.xn
` |-  ( ph -> -. X e. ( N ` { Y , Z } ) )`
21 hdmap1l6d.yz
` |-  ( ph -> ( N ` { Y } ) = ( N ` { Z } ) )`
22 hdmap1l6d.y
` |-  ( ph -> Y e. ( V \ { .0. } ) )`
23 hdmap1l6d.z
` |-  ( ph -> Z e. ( V \ { .0. } ) )`
24 hdmap1l6d.w
` |-  ( ph -> w e. ( V \ { .0. } ) )`
25 hdmap1l6d.wn
` |-  ( ph -> -. w e. ( N ` { X , Y } ) )`
26 1 2 16 dvhlvec
` |-  ( ph -> U e. LVec )`
` |-  ( ph -> Y e. V )`
` |-  ( ph -> w e. V )`
` |-  ( ph -> X e. V )`
` |-  ( ph -> Z e. V )`
31 3 7 26 29 27 30 20 lspindpi
` |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) )`
32 31 simpld
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
33 3 6 7 26 18 27 28 32 25 lspindp1
` |-  ( ph -> ( ( N ` { w } ) =/= ( N ` { Y } ) /\ -. X e. ( N ` { w , Y } ) ) )`
34 33 simprd
` |-  ( ph -> -. X e. ( N ` { w , Y } ) )`
35 3 7 26 28 29 27 25 lspindpi
` |-  ( ph -> ( ( N ` { w } ) =/= ( N ` { X } ) /\ ( N ` { w } ) =/= ( N ` { Y } ) ) )`
36 35 simprd
` |-  ( ph -> ( N ` { w } ) =/= ( N ` { Y } ) )`
37 eqidd
` |-  ( ph -> ( I ` <. X , F , w >. ) = ( I ` <. X , F , w >. ) )`
38 eqidd
` |-  ( ph -> ( I ` <. X , F , Y >. ) = ( I ` <. X , F , Y >. ) )`
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 24 22 34 36 37 38 hdmap1l6a
` |-  ( ph -> ( I ` <. X , F , ( w .+ Y ) >. ) = ( ( I ` <. X , F , w >. ) .+b ( I ` <. X , F , Y >. ) ) )`