Metamath Proof Explorer


Theorem mapdh8e

Description: Part of Part (8) in Baer p. 48. Eliminate w . (Contributed by NM, 10-May-2015)

Ref Expression
Hypotheses mapdh8a.h H = LHyp K
mapdh8a.u U = DVecH K W
mapdh8a.v V = Base U
mapdh8a.s - ˙ = - U
mapdh8a.o 0 ˙ = 0 U
mapdh8a.n N = LSpan U
mapdh8a.c C = LCDual K W
mapdh8a.d D = Base C
mapdh8a.r R = - C
mapdh8a.q Q = 0 C
mapdh8a.j J = LSpan C
mapdh8a.m M = mapd K W
mapdh8a.i I = x V if 2 nd x = 0 ˙ Q ι h D | M N 2 nd x = J h M N 1 st 1 st x - ˙ 2 nd x = J 2 nd 1 st x R h
mapdh8a.k φ K HL W H
mapdh8e.f φ F D
mapdh8e.mn φ M N X = J F
mapdh8e.eg φ I X F Y = G
mapdh8e.x φ X V 0 ˙
mapdh8e.y φ Y V 0 ˙
mapdh8e.t φ T V 0 ˙
mapdh8e.xy φ N X N Y
mapdh8e.xt φ N X N T
mapdh8e.yt φ N Y N T
mapdh8e.e φ X N Y T
Assertion mapdh8e φ I Y G T = I X F T

Proof

Step Hyp Ref Expression
1 mapdh8a.h H = LHyp K
2 mapdh8a.u U = DVecH K W
3 mapdh8a.v V = Base U
4 mapdh8a.s - ˙ = - U
5 mapdh8a.o 0 ˙ = 0 U
6 mapdh8a.n N = LSpan U
7 mapdh8a.c C = LCDual K W
8 mapdh8a.d D = Base C
9 mapdh8a.r R = - C
10 mapdh8a.q Q = 0 C
11 mapdh8a.j J = LSpan C
12 mapdh8a.m M = mapd K W
13 mapdh8a.i I = x V if 2 nd x = 0 ˙ Q ι h D | M N 2 nd x = J h M N 1 st 1 st x - ˙ 2 nd x = J 2 nd 1 st x R h
14 mapdh8a.k φ K HL W H
15 mapdh8e.f φ F D
16 mapdh8e.mn φ M N X = J F
17 mapdh8e.eg φ I X F Y = G
18 mapdh8e.x φ X V 0 ˙
19 mapdh8e.y φ Y V 0 ˙
20 mapdh8e.t φ T V 0 ˙
21 mapdh8e.xy φ N X N Y
22 mapdh8e.xt φ N X N T
23 mapdh8e.yt φ N Y N T
24 mapdh8e.e φ X N Y T
25 18 eldifad φ X V
26 19 eldifad φ Y V
27 1 2 3 6 14 25 26 dvh3dim φ w V ¬ w N X Y
28 14 3ad2ant1 φ w V ¬ w N X Y K HL W H
29 15 3ad2ant1 φ w V ¬ w N X Y F D
30 16 3ad2ant1 φ w V ¬ w N X Y M N X = J F
31 17 3ad2ant1 φ w V ¬ w N X Y I X F Y = G
32 18 3ad2ant1 φ w V ¬ w N X Y X V 0 ˙
33 19 3ad2ant1 φ w V ¬ w N X Y Y V 0 ˙
34 20 3ad2ant1 φ w V ¬ w N X Y T V 0 ˙
35 23 3ad2ant1 φ w V ¬ w N X Y N Y N T
36 eqid LSubSp U = LSubSp U
37 1 2 14 dvhlmod φ U LMod
38 37 3ad2ant1 φ w V ¬ w N X Y U LMod
39 3 36 6 37 25 26 lspprcl φ N X Y LSubSp U
40 39 3ad2ant1 φ w V ¬ w N X Y N X Y LSubSp U
41 simp2 φ w V ¬ w N X Y w V
42 simp3 φ w V ¬ w N X Y ¬ w N X Y
43 5 36 38 40 41 42 lssneln0 φ w V ¬ w N X Y w V 0 ˙
44 1 2 14 dvhlvec φ U LVec
45 20 eldifad φ T V
46 prcom Y T = T Y
47 46 fveq2i N Y T = N T Y
48 24 47 eleqtrdi φ X N T Y
49 3 5 6 44 18 45 26 21 48 lspexch φ T N X Y
50 36 6 37 39 49 lspsnel5a φ N T N X Y
51 50 3ad2ant1 φ w V ¬ w N X Y N T N X Y
52 37 adantr φ w V U LMod
53 39 adantr φ w V N X Y LSubSp U
54 simpr φ w V w V
55 3 36 6 52 53 54 lspsnel5 φ w V w N X Y N w N X Y
56 55 biimprd φ w V N w N X Y w N X Y
57 56 con3d φ w V ¬ w N X Y ¬ N w N X Y
58 57 3impia φ w V ¬ w N X Y ¬ N w N X Y
59 nssne2 N T N X Y ¬ N w N X Y N T N w
60 51 58 59 syl2anc φ w V ¬ w N X Y N T N w
61 60 necomd φ w V ¬ w N X Y N w N T
62 22 3ad2ant1 φ w V ¬ w N X Y N X N T
63 44 3ad2ant1 φ w V ¬ w N X Y U LVec
64 25 3ad2ant1 φ w V ¬ w N X Y X V
65 26 3ad2ant1 φ w V ¬ w N X Y Y V
66 3 6 63 41 64 65 42 lspindpi φ w V ¬ w N X Y N w N X N w N Y
67 66 simprd φ w V ¬ w N X Y N w N Y
68 67 necomd φ w V ¬ w N X Y N Y N w
69 21 3ad2ant1 φ w V ¬ w N X Y N X N Y
70 3 5 6 63 32 65 41 69 42 lspindp2l φ w V ¬ w N X Y N Y N w ¬ X N Y w
71 70 simprd φ w V ¬ w N X Y ¬ X N Y w
72 1 2 3 4 5 6 7 8 9 10 11 12 13 28 29 30 31 32 33 34 35 43 61 62 68 71 mapdh8d φ w V ¬ w N X Y I Y G T = I X F T
73 72 rexlimdv3a φ w V ¬ w N X Y I Y G T = I X F T
74 27 73 mpd φ I Y G T = I X F T