Metamath Proof Explorer

Theorem mapdh8ad

Description: Part of Part (8) in Baer p. 48. (Contributed by NM, 13-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
mapdh8ac.f ⊢ φ → F ∈ D
mapdh8ac.mn ⊢ φ → M ⁡ N ⁡ X = J ⁡ F
mapdh8ac.eg ⊢ φ → I ⁡ X F Y = G
mapdh8ac.ee ⊢ φ → I ⁡ X F Z = E
mapdh8ac.x ⊢ φ → X ∈ V ∖ 0 ˙
mapdh8ac.y ⊢ φ → Y ∈ V ∖ 0 ˙
mapdh8ac.z ⊢ φ → Z ∈ V ∖ 0 ˙
mapdh8ac.t ⊢ φ → T ∈ V ∖ 0 ˙
mapdh8ac.yn ⊢ φ → N ⁡ X = N ⁡ T
mapdh8ad.xy ⊢ φ → N ⁡ X ≠ N ⁡ Y
mapdh8ad.xz ⊢ φ → N ⁡ X ≠ N ⁡ Z
Assertion mapdh8ad ⊢ φ → I ⁡ Y G T = I ⁡ Z E 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 mapdh8ac.f ⊢ φ → F ∈ D
16 mapdh8ac.mn ⊢ φ → M ⁡ N ⁡ X = J ⁡ F
17 mapdh8ac.eg ⊢ φ → I ⁡ X F Y = G
18 mapdh8ac.ee ⊢ φ → I ⁡ X F Z = E
19 mapdh8ac.x ⊢ φ → X ∈ V ∖ 0 ˙
20 mapdh8ac.y ⊢ φ → Y ∈ V ∖ 0 ˙
21 mapdh8ac.z ⊢ φ → Z ∈ V ∖ 0 ˙
22 mapdh8ac.t ⊢ φ → T ∈ V ∖ 0 ˙
23 mapdh8ac.yn ⊢ φ → N ⁡ X = N ⁡ T
24 mapdh8ad.xy ⊢ φ → N ⁡ X ≠ N ⁡ Y
25 mapdh8ad.xz ⊢ φ → N ⁡ X ≠ N ⁡ Z
26 19 eldifad ⊢ φ → X ∈ V
27 20 eldifad ⊢ φ → Y ∈ V
28 21 eldifad ⊢ φ → Z ∈ V
29 1 2 3 6 14 26 27 28 dvh3dim2 ⊢ φ → ∃ w ∈ V ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z
30 14 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → K ∈ HL ∧ W ∈ H
31 15 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → F ∈ D
32 16 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → M ⁡ N ⁡ X = J ⁡ F
33 17 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → I ⁡ X F Y = G
34 18 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → I ⁡ X F Z = E
35 19 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → X ∈ V ∖ 0 ˙
36 20 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → Y ∈ V ∖ 0 ˙
37 21 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → Z ∈ V ∖ 0 ˙
38 22 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → T ∈ V ∖ 0 ˙
39 23 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → N ⁡ X = N ⁡ T
40 eqidd ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → I ⁡ X F w = I ⁡ X F w
41 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
42 1 2 14 dvhlmod ⊢ φ → U ∈ LMod
43 42 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → U ∈ LMod
44 3 41 6 42 26 27 lspprcl ⊢ φ → N ⁡ X Y ∈ LSubSp ⁡ U
45 44 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → N ⁡ X Y ∈ LSubSp ⁡ U
46 simp2 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → w ∈ V
47 simp3l ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → ¬ w ∈ N ⁡ X Y
48 5 41 43 45 46 47 lssneln0 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → w ∈ V ∖ 0 ˙
49 1 2 14 dvhlvec ⊢ φ → U ∈ LVec
50 49 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → U ∈ LVec
51 26 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → X ∈ V
52 27 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → Y ∈ V
53 3 6 50 46 51 52 47 lspindpi ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → N ⁡ w ≠ N ⁡ X ∧ N ⁡ w ≠ N ⁡ Y
54 53 simprd ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → N ⁡ w ≠ N ⁡ Y
55 54 necomd ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → N ⁡ Y ≠ N ⁡ w
56 simpl1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → φ
57 56 49 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → U ∈ LVec
58 56 19 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → X ∈ V ∖ 0 ˙
59 simpl2 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → w ∈ V
60 56 27 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → Y ∈ V
61 56 24 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → N ⁡ X ≠ N ⁡ Y
62 simpr ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → X ∈ N ⁡ Y w
63 prcom ⊢ Y w = w Y
64 63 fveq2i ⊢ N ⁡ Y w = N ⁡ w Y
65 62 64 eleqtrdi ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → X ∈ N ⁡ w Y
66 3 5 6 57 58 59 60 61 65 lspexch ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ Y w → w ∈ N ⁡ X Y
67 47 66 mtand ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → ¬ X ∈ N ⁡ Y w
68 28 3ad2ant1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → Z ∈ V
69 simp3r ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → ¬ w ∈ N ⁡ X Z
70 3 6 50 46 51 68 69 lspindpi ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → N ⁡ w ≠ N ⁡ X ∧ N ⁡ w ≠ N ⁡ Z
71 70 simprd ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → N ⁡ w ≠ N ⁡ Z
72 simpl1 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → φ
73 72 49 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → U ∈ LVec
74 72 19 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → X ∈ V ∖ 0 ˙
75 simpl2 ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → w ∈ V
76 72 28 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → Z ∈ V
77 72 25 syl ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → N ⁡ X ≠ N ⁡ Z
78 simpr ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → X ∈ N ⁡ w Z
79 3 5 6 73 74 75 76 77 78 lspexch ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z ∧ X ∈ N ⁡ w Z → w ∈ N ⁡ X Z
80 69 79 mtand ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → ¬ X ∈ N ⁡ w Z
81 1 2 3 4 5 6 7 8 9 10 11 12 13 30 31 32 33 34 35 36 37 38 39 40 48 55 67 71 80 mapdh8ac ⊢ φ ∧ w ∈ V ∧ ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → I ⁡ Y G T = I ⁡ Z E T
82 81 rexlimdv3a ⊢ φ → ∃ w ∈ V ¬ w ∈ N ⁡ X Y ∧ ¬ w ∈ N ⁡ X Z → I ⁡ Y G T = I ⁡ Z E T
83 29 82 mpd ⊢ φ → I ⁡ Y G T = I ⁡ Z E T