Metamath Proof Explorer


Theorem mapdh9aOLDN

Description: Lemma for part (9) in Baer p. 48. (Contributed by NM, 14-May-2015) (New usage is discouraged.)

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
mapdh8h.f φ F D
mapdh8h.mn φ M N X = J F
mapdh9a.x φ X V 0 ˙
mapdh9a.t φ T V
Assertion mapdh9aOLDN φ ∃! y D z V ¬ z N X T y = I z I X F z 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 mapdh8h.f φ F D
16 mapdh8h.mn φ M N X = J F
17 mapdh9a.x φ X V 0 ˙
18 mapdh9a.t φ T V
19 14 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T K HL W H
20 15 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T F D
21 16 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T M N X = J F
22 17 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T X V 0 ˙
23 eqid LSubSp U = LSubSp U
24 1 2 14 dvhlmod φ U LMod
25 24 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T U LMod
26 17 eldifad φ X V
27 3 23 6 24 26 18 lspprcl φ N X T LSubSp U
28 27 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T N X T LSubSp U
29 simp2l φ z V w V ¬ z N X T ¬ w N X T z V
30 simp3l φ z V w V ¬ z N X T ¬ w N X T ¬ z N X T
31 5 23 25 28 29 30 lssneln0 φ z V w V ¬ z N X T ¬ w N X T z V 0 ˙
32 simp2r φ z V w V ¬ z N X T ¬ w N X T w V
33 simp3r φ z V w V ¬ z N X T ¬ w N X T ¬ w N X T
34 5 23 25 28 32 33 lssneln0 φ z V w V ¬ z N X T ¬ w N X T w V 0 ˙
35 1 2 14 dvhlvec φ U LVec
36 35 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T U LVec
37 26 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T X V
38 18 3ad2ant1 φ z V w V ¬ z N X T ¬ w N X T T V
39 3 6 36 29 37 38 30 lspindpi φ z V w V ¬ z N X T ¬ w N X T N z N X N z N T
40 39 simpld φ z V w V ¬ z N X T ¬ w N X T N z N X
41 40 necomd φ z V w V ¬ z N X T ¬ w N X T N X N z
42 3 6 36 32 37 38 33 lspindpi φ z V w V ¬ z N X T ¬ w N X T N w N X N w N T
43 42 simpld φ z V w V ¬ z N X T ¬ w N X T N w N X
44 43 necomd φ z V w V ¬ z N X T ¬ w N X T N X N w
45 39 simprd φ z V w V ¬ z N X T ¬ w N X T N z N T
46 42 simprd φ z V w V ¬ z N X T ¬ w N X T N w N T
47 1 2 3 4 5 6 7 8 9 10 11 12 13 19 20 21 22 31 34 41 44 45 46 38 mapdh8 φ z V w V ¬ z N X T ¬ w N X T I z I X F z T = I w I X F w T
48 47 3exp φ z V w V ¬ z N X T ¬ w N X T I z I X F z T = I w I X F w T
49 48 ralrimivv φ z V w V ¬ z N X T ¬ w N X T I z I X F z T = I w I X F w T
50 1 2 3 6 14 26 18 dvh3dim φ z V ¬ z N X T
51 14 ad2antrr φ z V ¬ z N X T K HL W H
52 15 ad2antrr φ z V ¬ z N X T F D
53 16 ad2antrr φ z V ¬ z N X T M N X = J F
54 17 ad2antrr φ z V ¬ z N X T X V 0 ˙
55 simplr φ z V ¬ z N X T z V
56 35 ad2antrr φ z V ¬ z N X T U LVec
57 26 ad2antrr φ z V ¬ z N X T X V
58 18 ad2antrr φ z V ¬ z N X T T V
59 simpr φ z V ¬ z N X T ¬ z N X T
60 3 6 56 55 57 58 59 lspindpi φ z V ¬ z N X T N z N X N z N T
61 60 simpld φ z V ¬ z N X T N z N X
62 61 necomd φ z V ¬ z N X T N X N z
63 10 13 1 12 2 3 4 5 6 7 8 9 11 51 52 53 54 55 62 mapdhcl φ z V ¬ z N X T I X F z D
64 eqidd φ z V ¬ z N X T I X F z = I X F z
65 24 ad2antrr φ z V ¬ z N X T U LMod
66 27 ad2antrr φ z V ¬ z N X T N X T LSubSp U
67 5 23 65 66 55 59 lssneln0 φ z V ¬ z N X T z V 0 ˙
68 10 13 1 12 2 3 4 5 6 7 8 9 11 51 52 53 54 67 63 62 mapdheq φ z V ¬ z N X T I X F z = I X F z M N z = J I X F z M N X - ˙ z = J F R I X F z
69 64 68 mpbid φ z V ¬ z N X T M N z = J I X F z M N X - ˙ z = J F R I X F z
70 69 simpld φ z V ¬ z N X T M N z = J I X F z
71 60 simprd φ z V ¬ z N X T N z N T
72 10 13 1 12 2 3 4 5 6 7 8 9 11 51 63 70 67 58 71 mapdhcl φ z V ¬ z N X T I z I X F z T D
73 72 ex φ z V ¬ z N X T I z I X F z T D
74 73 ancld φ z V ¬ z N X T ¬ z N X T I z I X F z T D
75 74 reximdva φ z V ¬ z N X T z V ¬ z N X T I z I X F z T D
76 50 75 mpd φ z V ¬ z N X T I z I X F z T D
77 eleq1w z = w z N X T w N X T
78 77 notbid z = w ¬ z N X T ¬ w N X T
79 oteq1 z = w z I X F z T = w I X F z T
80 oteq3 z = w X F z = X F w
81 80 fveq2d z = w I X F z = I X F w
82 81 oteq2d z = w w I X F z T = w I X F w T
83 79 82 eqtrd z = w z I X F z T = w I X F w T
84 83 fveq2d z = w I z I X F z T = I w I X F w T
85 78 84 reusv3 z V ¬ z N X T I z I X F z T D z V w V ¬ z N X T ¬ w N X T I z I X F z T = I w I X F w T y D z V ¬ z N X T y = I z I X F z T
86 76 85 syl φ z V w V ¬ z N X T ¬ w N X T I z I X F z T = I w I X F w T y D z V ¬ z N X T y = I z I X F z T
87 49 86 mpbid φ y D z V ¬ z N X T y = I z I X F z T
88 reusv1 z V ¬ z N X T ∃! y D z V ¬ z N X T y = I z I X F z T y D z V ¬ z N X T y = I z I X F z T
89 50 88 syl φ ∃! y D z V ¬ z N X T y = I z I X F z T y D z V ¬ z N X T y = I z I X F z T
90 87 89 mpbird φ ∃! y D z V ¬ z N X T y = I z I X F z T