# Metamath Proof Explorer

## Theorem hdmap1l6e

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 hdmap1l6e
`|- ( ph -> ( I ` <. X , F , ( ( w .+ Y ) .+ Z ) >. ) = ( ( I ` <. X , F , ( w .+ Y ) >. ) .+b ( I ` <. X , F , Z >. ) ) )`

### 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 dvhlmod
` |-  ( ph -> U e. LMod )`
` |-  ( ph -> w e. V )`
` |-  ( ph -> Y e. V )`
29 3 4 lmodvacl
` |-  ( ( U e. LMod /\ w e. V /\ Y e. V ) -> ( w .+ Y ) e. V )`
30 26 27 28 29 syl3anc
` |-  ( ph -> ( w .+ Y ) e. V )`
31 1 2 16 dvhlvec
` |-  ( ph -> U e. LVec )`
` |-  ( ph -> X e. V )`
33 3 7 31 27 32 28 25 lspindpi
` |-  ( ph -> ( ( N ` { w } ) =/= ( N ` { X } ) /\ ( N ` { w } ) =/= ( N ` { Y } ) ) )`
34 33 simprd
` |-  ( ph -> ( N ` { w } ) =/= ( N ` { Y } ) )`
35 3 4 6 7 26 27 28 34 lmodindp1
` |-  ( ph -> ( w .+ Y ) =/= .0. )`
36 eldifsn
` |-  ( ( w .+ Y ) e. ( V \ { .0. } ) <-> ( ( w .+ Y ) e. V /\ ( w .+ Y ) =/= .0. ) )`
37 30 35 36 sylanbrc
` |-  ( ph -> ( w .+ Y ) e. ( V \ { .0. } ) )`
` |-  ( ph -> Z e. V )`
39 3 7 31 32 28 38 20 lspindpi
` |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ ( N ` { X } ) =/= ( N ` { Z } ) ) )`
40 39 simpld
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
41 3 4 6 7 31 18 22 23 24 21 40 25 mapdindp3
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { ( w .+ Y ) } ) )`
42 3 4 6 7 31 18 22 23 24 21 40 25 mapdindp4
` |-  ( ph -> -. Z e. ( N ` { X , ( w .+ Y ) } ) )`
43 3 6 7 31 18 30 38 41 42 lspindp1
` |-  ( ph -> ( ( N ` { Z } ) =/= ( N ` { ( w .+ Y ) } ) /\ -. X e. ( N ` { Z , ( w .+ Y ) } ) ) )`
44 43 simprd
` |-  ( ph -> -. X e. ( N ` { Z , ( w .+ Y ) } ) )`
45 prcom
` |-  { ( w .+ Y ) , Z } = { Z , ( w .+ Y ) }`
46 45 fveq2i
` |-  ( N ` { ( w .+ Y ) , Z } ) = ( N ` { Z , ( w .+ Y ) } )`
47 46 eleq2i
` |-  ( X e. ( N ` { ( w .+ Y ) , Z } ) <-> X e. ( N ` { Z , ( w .+ Y ) } ) )`
48 44 47 sylnibr
` |-  ( ph -> -. X e. ( N ` { ( w .+ Y ) , Z } ) )`
49 3 7 31 38 32 30 42 lspindpi
` |-  ( ph -> ( ( N ` { Z } ) =/= ( N ` { X } ) /\ ( N ` { Z } ) =/= ( N ` { ( w .+ Y ) } ) ) )`
50 49 simprd
` |-  ( ph -> ( N ` { Z } ) =/= ( N ` { ( w .+ Y ) } ) )`
51 50 necomd
` |-  ( ph -> ( N ` { ( w .+ Y ) } ) =/= ( N ` { Z } ) )`
52 eqidd
` |-  ( ph -> ( I ` <. X , F , ( w .+ Y ) >. ) = ( I ` <. X , F , ( w .+ Y ) >. ) )`
53 eqidd
` |-  ( ph -> ( I ` <. X , F , Z >. ) = ( I ` <. X , F , Z >. ) )`
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 37 23 48 51 52 53 hdmap1l6a
` |-  ( ph -> ( I ` <. X , F , ( ( w .+ Y ) .+ Z ) >. ) = ( ( I ` <. X , F , ( w .+ Y ) >. ) .+b ( I ` <. X , F , Z >. ) ) )`