Metamath Proof Explorer


Theorem mapdpglem13

Description: Lemma for mapdpg . (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses mapdpglem.h H = LHyp K
mapdpglem.m M = mapd K W
mapdpglem.u U = DVecH K W
mapdpglem.v V = Base U
mapdpglem.s - ˙ = - U
mapdpglem.n N = LSpan U
mapdpglem.c C = LCDual K W
mapdpglem.k φ K HL W H
mapdpglem.x φ X V
mapdpglem.y φ Y V
mapdpglem1.p ˙ = LSSum C
mapdpglem2.j J = LSpan C
mapdpglem3.f F = Base C
mapdpglem3.te φ t M N X ˙ M N Y
mapdpglem3.a A = Scalar U
mapdpglem3.b B = Base A
mapdpglem3.t · ˙ = C
mapdpglem3.r R = - C
mapdpglem3.g φ G F
mapdpglem3.e φ M N X = J G
mapdpglem4.q Q = 0 U
mapdpglem.ne φ N X N Y
mapdpglem4.jt φ M N X - ˙ Y = J t
mapdpglem4.z 0 ˙ = 0 A
mapdpglem4.g4 φ g B
mapdpglem4.z4 φ z M N Y
mapdpglem4.t4 φ t = g · ˙ G R z
mapdpglem4.xn φ X Q
mapdpglem12.yn φ Y Q
mapdpglem12.g0 φ z = 0 C
Assertion mapdpglem13 φ N X - ˙ Y N X

Proof

Step Hyp Ref Expression
1 mapdpglem.h H = LHyp K
2 mapdpglem.m M = mapd K W
3 mapdpglem.u U = DVecH K W
4 mapdpglem.v V = Base U
5 mapdpglem.s - ˙ = - U
6 mapdpglem.n N = LSpan U
7 mapdpglem.c C = LCDual K W
8 mapdpglem.k φ K HL W H
9 mapdpglem.x φ X V
10 mapdpglem.y φ Y V
11 mapdpglem1.p ˙ = LSSum C
12 mapdpglem2.j J = LSpan C
13 mapdpglem3.f F = Base C
14 mapdpglem3.te φ t M N X ˙ M N Y
15 mapdpglem3.a A = Scalar U
16 mapdpglem3.b B = Base A
17 mapdpglem3.t · ˙ = C
18 mapdpglem3.r R = - C
19 mapdpglem3.g φ G F
20 mapdpglem3.e φ M N X = J G
21 mapdpglem4.q Q = 0 U
22 mapdpglem.ne φ N X N Y
23 mapdpglem4.jt φ M N X - ˙ Y = J t
24 mapdpglem4.z 0 ˙ = 0 A
25 mapdpglem4.g4 φ g B
26 mapdpglem4.z4 φ z M N Y
27 mapdpglem4.t4 φ t = g · ˙ G R z
28 mapdpglem4.xn φ X Q
29 mapdpglem12.yn φ Y Q
30 mapdpglem12.g0 φ z = 0 C
31 eqid LSubSp C = LSubSp C
32 1 7 8 lcdlmod φ C LMod
33 eqid LSubSp U = LSubSp U
34 1 3 8 dvhlmod φ U LMod
35 4 33 6 lspsncl U LMod X V N X LSubSp U
36 34 9 35 syl2anc φ N X LSubSp U
37 1 2 3 33 7 31 8 36 mapdcl2 φ M N X LSubSp C
38 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 26 27 28 29 30 mapdpglem12 φ t M N X
39 31 12 32 37 38 lspsnel5a φ J t M N X
40 23 39 eqsstrd φ M N X - ˙ Y M N X
41 4 5 lmodvsubcl U LMod X V Y V X - ˙ Y V
42 34 9 10 41 syl3anc φ X - ˙ Y V
43 4 33 6 lspsncl U LMod X - ˙ Y V N X - ˙ Y LSubSp U
44 34 42 43 syl2anc φ N X - ˙ Y LSubSp U
45 1 3 33 2 8 44 36 mapdord φ M N X - ˙ Y M N X N X - ˙ Y N X
46 40 45 mpbid φ N X - ˙ Y N X