Metamath Proof Explorer


Theorem hdmap1l6c

Description: Lemmma for hdmap1l6 . (Contributed by NM, 24-Apr-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
hdmap1l6c.y φ Y V
hdmap1l6c.z φ Z = 0 ˙
hdmap1l6c.ne φ ¬ X N Y Z
Assertion hdmap1l6c φ 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 hdmap1l6c.y φ Y V
21 hdmap1l6c.z φ Z = 0 ˙
22 hdmap1l6c.ne φ ¬ X N Y Z
23 1 8 16 lcdlmod φ C LMod
24 lmodgrp C LMod C Grp
25 23 24 syl φ C Grp
26 1 2 16 dvhlvec φ U LVec
27 18 eldifad φ X V
28 1 2 16 dvhlmod φ U LMod
29 3 6 lmod0vcl U LMod 0 ˙ V
30 28 29 syl φ 0 ˙ V
31 21 30 eqeltrd φ Z V
32 3 7 26 27 20 31 22 lspindpi φ N X N Y N X N Z
33 32 simpld φ N X N Y
34 1 2 3 6 7 8 9 13 14 15 16 17 19 33 18 20 hdmap1cl φ I X F Y D
35 9 10 12 grprid C Grp I X F Y D I X F Y ˙ Q = I X F Y
36 25 34 35 syl2anc φ I X F Y ˙ Q = I X F Y
37 21 oteq3d φ X F Z = X F 0 ˙
38 37 fveq2d φ I X F Z = I X F 0 ˙
39 1 2 3 6 8 9 12 15 16 17 27 hdmap1val0 φ I X F 0 ˙ = Q
40 38 39 eqtrd φ I X F Z = Q
41 40 oveq2d φ I X F Y ˙ I X F Z = I X F Y ˙ Q
42 21 oveq2d φ Y + ˙ Z = Y + ˙ 0 ˙
43 lmodgrp U LMod U Grp
44 28 43 syl φ U Grp
45 3 4 6 grprid U Grp Y V Y + ˙ 0 ˙ = Y
46 44 20 45 syl2anc φ Y + ˙ 0 ˙ = Y
47 42 46 eqtrd φ Y + ˙ Z = Y
48 47 oteq3d φ X F Y + ˙ Z = X F Y
49 48 fveq2d φ I X F Y + ˙ Z = I X F Y
50 36 41 49 3eqtr4rd φ I X F Y + ˙ Z = I X F Y ˙ I X F Z