# Metamath Proof Explorer

## Theorem hdmap1l6a

Description: Lemma for hdmap1l6 . Part (6) in Baer p. 47, case 1. (Contributed by NM, 23-Apr-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 } ) )`
hdmap1l6e.y
`|- ( ph -> Y e. ( V \ { .0. } ) )`
hdmap1l6e.z
`|- ( ph -> Z e. ( V \ { .0. } ) )`
hdmap1l6e.xn
`|- ( ph -> -. X e. ( N ` { Y , Z } ) )`
hdmap1l6.yz
`|- ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )`
hdmap1l6.fg
`|- ( ph -> ( I ` <. X , F , Y >. ) = G )`
hdmap1l6.fe
`|- ( ph -> ( I ` <. X , F , Z >. ) = E )`
Assertion hdmap1l6a
`|- ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , 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 hdmap1l6e.y
` |-  ( ph -> Y e. ( V \ { .0. } ) )`
21 hdmap1l6e.z
` |-  ( ph -> Z e. ( V \ { .0. } ) )`
22 hdmap1l6e.xn
` |-  ( ph -> -. X e. ( N ` { Y , Z } ) )`
23 hdmap1l6.yz
` |-  ( ph -> ( N ` { Y } ) =/= ( N ` { Z } ) )`
24 hdmap1l6.fg
` |-  ( ph -> ( I ` <. X , F , Y >. ) = G )`
25 hdmap1l6.fe
` |-  ( ph -> ( I ` <. X , F , Z >. ) = E )`
26 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 hdmap1l6lem2
` |-  ( ph -> ( M ` ( N ` { ( Y .+ Z ) } ) ) = ( L ` { ( G .+b E ) } ) )`
27 24 25 oveq12d
` |-  ( ph -> ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) = ( G .+b E ) )`
28 27 sneqd
` |-  ( ph -> { ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) } = { ( G .+b E ) } )`
29 28 fveq2d
` |-  ( ph -> ( L ` { ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) } ) = ( L ` { ( G .+b E ) } ) )`
30 26 29 eqtr4d
` |-  ( ph -> ( M ` ( N ` { ( Y .+ Z ) } ) ) = ( L ` { ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) } ) )`
31 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 hdmap1l6lem1
` |-  ( ph -> ( M ` ( N ` { ( X .- ( Y .+ Z ) ) } ) ) = ( L ` { ( F R ( G .+b E ) ) } ) )`
32 27 oveq2d
` |-  ( ph -> ( F R ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) ) = ( F R ( G .+b E ) ) )`
33 32 sneqd
` |-  ( ph -> { ( F R ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) ) } = { ( F R ( G .+b E ) ) } )`
34 33 fveq2d
` |-  ( ph -> ( L ` { ( F R ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) ) } ) = ( L ` { ( F R ( G .+b E ) ) } ) )`
35 31 34 eqtr4d
` |-  ( ph -> ( M ` ( N ` { ( X .- ( Y .+ Z ) ) } ) ) = ( L ` { ( F R ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) ) } ) )`
36 1 2 16 dvhlmod
` |-  ( ph -> U e. LMod )`
` |-  ( ph -> Y e. V )`
` |-  ( ph -> Z e. V )`
39 3 4 lmodvacl
` |-  ( ( U e. LMod /\ Y e. V /\ Z e. V ) -> ( Y .+ Z ) e. V )`
40 36 37 38 39 syl3anc
` |-  ( ph -> ( Y .+ Z ) e. V )`
41 3 4 6 7 36 37 38 23 lmodindp1
` |-  ( ph -> ( Y .+ Z ) =/= .0. )`
42 eldifsn
` |-  ( ( Y .+ Z ) e. ( V \ { .0. } ) <-> ( ( Y .+ Z ) e. V /\ ( Y .+ Z ) =/= .0. ) )`
43 40 41 42 sylanbrc
` |-  ( ph -> ( Y .+ Z ) e. ( V \ { .0. } ) )`
44 1 8 16 lcdlmod
` |-  ( ph -> C e. LMod )`
45 1 2 16 dvhlvec
` |-  ( ph -> U e. LVec )`
` |-  ( ph -> X e. V )`
47 3 6 7 45 37 21 46 23 22 lspindp2
` |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) /\ -. Z e. ( N ` { X , Y } ) ) )`
48 47 simpld
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
49 1 2 3 6 7 8 9 13 14 15 16 17 19 48 18 37 hdmap1cl
` |-  ( ph -> ( I ` <. X , F , Y >. ) e. D )`
50 3 6 7 45 20 38 46 23 22 lspindp1
` |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Z } ) /\ -. Y e. ( N ` { X , Z } ) ) )`
51 50 simpld
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { Z } ) )`
52 1 2 3 6 7 8 9 13 14 15 16 17 19 51 18 38 hdmap1cl
` |-  ( ph -> ( I ` <. X , F , Z >. ) e. D )`
53 9 10 lmodvacl
` |-  ( ( C e. LMod /\ ( I ` <. X , F , Y >. ) e. D /\ ( I ` <. X , F , Z >. ) e. D ) -> ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) e. D )`
54 44 49 52 53 syl3anc
` |-  ( ph -> ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) e. D )`
55 eqid
` |-  ( LSubSp ` U ) = ( LSubSp ` U )`
56 3 55 7 36 37 38 lspprcl
` |-  ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` U ) )`
57 3 4 7 36 37 38 lspprvacl
` |-  ( ph -> ( Y .+ Z ) e. ( N ` { Y , Z } ) )`
58 55 7 36 56 57 lspsnel5a
` |-  ( ph -> ( N ` { ( Y .+ Z ) } ) C_ ( N ` { Y , Z } ) )`
59 3 55 7 36 56 46 lspsnel5
` |-  ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) )`
60 22 59 mtbid
` |-  ( ph -> -. ( N ` { X } ) C_ ( N ` { Y , Z } ) )`
61 nssne2
` |-  ( ( ( N ` { ( Y .+ Z ) } ) C_ ( N ` { Y , Z } ) /\ -. ( N ` { X } ) C_ ( N ` { Y , Z } ) ) -> ( N ` { ( Y .+ Z ) } ) =/= ( N ` { X } ) )`
62 58 60 61 syl2anc
` |-  ( ph -> ( N ` { ( Y .+ Z ) } ) =/= ( N ` { X } ) )`
63 62 necomd
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { ( Y .+ Z ) } ) )`
64 1 2 3 5 6 7 8 9 11 13 14 15 16 18 17 43 54 63 19 hdmap1eq
` |-  ( ph -> ( ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) <-> ( ( M ` ( N ` { ( Y .+ Z ) } ) ) = ( L ` { ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) } ) /\ ( M ` ( N ` { ( X .- ( Y .+ Z ) ) } ) ) = ( L ` { ( F R ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) ) } ) ) ) )`
65 30 35 64 mpbir2and
` |-  ( ph -> ( I ` <. X , F , ( Y .+ Z ) >. ) = ( ( I ` <. X , F , Y >. ) .+b ( I ` <. X , F , Z >. ) ) )`