Metamath Proof Explorer


Theorem hdmap1eulemOLDN

Description: Lemma for hdmap1euOLDN . TODO: combine with hdmap1euOLDN or at least share some hypotheses. (Contributed by NM, 15-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmap1eulem.h H = LHyp K
hdmap1eulem.u U = DVecH K W
hdmap1eulem.v V = Base U
hdmap1eulem.s - ˙ = - U
hdmap1eulem.o 0 ˙ = 0 U
hdmap1eulem.n N = LSpan U
hdmap1eulem.c C = LCDual K W
hdmap1eulem.d D = Base C
hdmap1eulem.r R = - C
hdmap1eulem.q Q = 0 C
hdmap1eulem.j J = LSpan C
hdmap1eulem.m M = mapd K W
hdmap1eulem.i I = HDMap1 K W
hdmap1eulem.k φ K HL W H
hdmap1eulem.mn φ M N X = J F
hdmap1eulem.x φ X V 0 ˙
hdmap1eulem.f φ F D
hdmap1eulem.y φ T V
hdmap1eulem.l L = 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
Assertion hdmap1eulemOLDN φ ∃! y D z V ¬ z N X T y = I z I X F z T

Proof

Step Hyp Ref Expression
1 hdmap1eulem.h H = LHyp K
2 hdmap1eulem.u U = DVecH K W
3 hdmap1eulem.v V = Base U
4 hdmap1eulem.s - ˙ = - U
5 hdmap1eulem.o 0 ˙ = 0 U
6 hdmap1eulem.n N = LSpan U
7 hdmap1eulem.c C = LCDual K W
8 hdmap1eulem.d D = Base C
9 hdmap1eulem.r R = - C
10 hdmap1eulem.q Q = 0 C
11 hdmap1eulem.j J = LSpan C
12 hdmap1eulem.m M = mapd K W
13 hdmap1eulem.i I = HDMap1 K W
14 hdmap1eulem.k φ K HL W H
15 hdmap1eulem.mn φ M N X = J F
16 hdmap1eulem.x φ X V 0 ˙
17 hdmap1eulem.f φ F D
18 hdmap1eulem.y φ T V
19 hdmap1eulem.l L = 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
20 1 2 3 4 5 6 7 8 9 10 11 12 19 14 17 15 16 18 mapdh9aOLDN φ ∃! y D z V ¬ z N X T y = L z L X F z T
21 14 ad2antrr φ z V ¬ z N X T K HL W H
22 16 ad2antrr φ z V ¬ z N X T X V 0 ˙
23 17 ad2antrr φ z V ¬ z N X T F D
24 simplr φ z V ¬ z N X T z V
25 1 2 3 4 5 6 7 8 9 10 11 12 13 21 22 23 24 19 hdmap1valc φ z V ¬ z N X T I X F z = L X F z
26 25 oteq2d φ z V ¬ z N X T z I X F z T = z L X F z T
27 26 fveq2d φ z V ¬ z N X T I z I X F z T = I z L X F z T
28 eqid LSubSp U = LSubSp U
29 1 2 14 dvhlmod φ U LMod
30 29 ad2antrr φ z V ¬ z N X T U LMod
31 16 eldifad φ X V
32 3 28 6 29 31 18 lspprcl φ N X T LSubSp U
33 32 ad2antrr φ z V ¬ z N X T N X T LSubSp U
34 simpr φ z V ¬ z N X T ¬ z N X T
35 5 28 30 33 24 34 lssneln0 φ z V ¬ z N X T z V 0 ˙
36 15 ad2antrr φ z V ¬ z N X T M N X = J F
37 1 2 14 dvhlvec φ U LVec
38 37 ad2antrr φ z V ¬ z N X T U LVec
39 31 ad2antrr φ z V ¬ z N X T X V
40 18 ad2antrr φ z V ¬ z N X T T V
41 3 6 38 24 39 40 34 lspindpi φ z V ¬ z N X T N z N X N z N T
42 41 simpld φ z V ¬ z N X T N z N X
43 42 necomd φ z V ¬ z N X T N X N z
44 10 19 1 12 2 3 4 5 6 7 8 9 11 21 23 36 22 24 43 mapdhcl φ z V ¬ z N X T L X F z D
45 1 2 3 4 5 6 7 8 9 10 11 12 13 21 35 44 40 19 hdmap1valc φ z V ¬ z N X T I z L X F z T = L z L X F z T
46 27 45 eqtrd φ z V ¬ z N X T I z I X F z T = L z L X F z T
47 46 eqeq2d φ z V ¬ z N X T y = I z I X F z T y = L z L X F z T
48 47 pm5.74da φ z V ¬ z N X T y = I z I X F z T ¬ z N X T y = L z L X F z T
49 48 ralbidva φ z V ¬ z N X T y = I z I X F z T z V ¬ z N X T y = L z L X F z T
50 49 reubidv φ ∃! 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 = L z L X F z T
51 20 50 mpbird φ ∃! y D z V ¬ z N X T y = I z I X F z T