Metamath Proof Explorer


Theorem hdmap1l6i

Description: Lemmma for hdmap1l6 . Eliminate auxiliary vector w . (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 + ˙ = + U
hdmap1l6.s - ˙ = - U
hdmap1l6c.o 0 ˙ = 0 U
hdmap1l6.n N = LSpan U
hdmap1l6.c C = LCDual K W
hdmap1l6.d D = Base C
hdmap1l6.a ˙ = + C
hdmap1l6.r R = - C
hdmap1l6.q Q = 0 C
hdmap1l6.l L = LSpan C
hdmap1l6.m M = mapd K W
hdmap1l6.i I = HDMap1 K W
hdmap1l6.k φ K HL W H
hdmap1l6.f φ F D
hdmap1l6cl.x φ X V 0 ˙
hdmap1l6.mn φ M N X = L F
hdmap1l6i.xn φ ¬ X N Y Z
hdmap1l6i.y φ Y V 0 ˙
hdmap1l6i.z φ Z V 0 ˙
hdmap1l6i.yz φ N Y = N Z
Assertion hdmap1l6i φ I X F Y + ˙ Z = I X F Y ˙ 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 + ˙ = + U
5 hdmap1l6.s - ˙ = - U
6 hdmap1l6c.o 0 ˙ = 0 U
7 hdmap1l6.n N = LSpan U
8 hdmap1l6.c C = LCDual K W
9 hdmap1l6.d D = Base C
10 hdmap1l6.a ˙ = + C
11 hdmap1l6.r R = - C
12 hdmap1l6.q Q = 0 C
13 hdmap1l6.l L = LSpan C
14 hdmap1l6.m M = mapd K W
15 hdmap1l6.i I = HDMap1 K W
16 hdmap1l6.k φ K HL W H
17 hdmap1l6.f φ F D
18 hdmap1l6cl.x φ X V 0 ˙
19 hdmap1l6.mn φ M N X = L F
20 hdmap1l6i.xn φ ¬ X N Y Z
21 hdmap1l6i.y φ Y V 0 ˙
22 hdmap1l6i.z φ Z V 0 ˙
23 hdmap1l6i.yz φ N Y = N Z
24 18 eldifad φ X V
25 21 eldifad φ Y V
26 1 2 3 7 16 24 25 dvh3dim φ w V ¬ w N X Y
27 16 3ad2ant1 φ w V ¬ w N X Y K HL W H
28 17 3ad2ant1 φ w V ¬ w N X Y F D
29 18 3ad2ant1 φ w V ¬ w N X Y X V 0 ˙
30 19 3ad2ant1 φ w V ¬ w N X Y M N X = L F
31 20 3ad2ant1 φ w V ¬ w N X Y ¬ X N Y Z
32 23 3ad2ant1 φ w V ¬ w N X Y N Y = N Z
33 21 3ad2ant1 φ w V ¬ w N X Y Y V 0 ˙
34 22 3ad2ant1 φ w V ¬ w N X Y Z V 0 ˙
35 eqid LSubSp U = LSubSp U
36 1 2 16 dvhlmod φ U LMod
37 36 3ad2ant1 φ w V ¬ w N X Y U LMod
38 3 35 7 36 24 25 lspprcl φ N X Y LSubSp U
39 38 3ad2ant1 φ w V ¬ w N X Y N X Y LSubSp U
40 simp2 φ w V ¬ w N X Y w V
41 simp3 φ w V ¬ w N X Y ¬ w N X Y
42 6 35 37 39 40 41 lssneln0 φ w V ¬ w N X Y w V 0 ˙
43 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 27 28 29 30 31 32 33 34 42 41 hdmap1l6h φ w V ¬ w N X Y I X F Y + ˙ Z = I X F Y ˙ I X F Z
44 43 rexlimdv3a φ w V ¬ w N X Y I X F Y + ˙ Z = I X F Y ˙ I X F Z
45 26 44 mpd φ I X F Y + ˙ Z = I X F Y ˙ I X F Z