Metamath Proof Explorer


Theorem hdmap1fval

Description: Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span J to the convention L for this section. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmap1val.h H = LHyp K
hdmap1fval.u U = DVecH K W
hdmap1fval.v V = Base U
hdmap1fval.s - ˙ = - U
hdmap1fval.o 0 ˙ = 0 U
hdmap1fval.n N = LSpan U
hdmap1fval.c C = LCDual K W
hdmap1fval.d D = Base C
hdmap1fval.r R = - C
hdmap1fval.q Q = 0 C
hdmap1fval.j J = LSpan C
hdmap1fval.m M = mapd K W
hdmap1fval.i I = HDMap1 K W
hdmap1fval.k φ K A W H
Assertion hdmap1fval φ I = x V × D × 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

Proof

Step Hyp Ref Expression
1 hdmap1val.h H = LHyp K
2 hdmap1fval.u U = DVecH K W
3 hdmap1fval.v V = Base U
4 hdmap1fval.s - ˙ = - U
5 hdmap1fval.o 0 ˙ = 0 U
6 hdmap1fval.n N = LSpan U
7 hdmap1fval.c C = LCDual K W
8 hdmap1fval.d D = Base C
9 hdmap1fval.r R = - C
10 hdmap1fval.q Q = 0 C
11 hdmap1fval.j J = LSpan C
12 hdmap1fval.m M = mapd K W
13 hdmap1fval.i I = HDMap1 K W
14 hdmap1fval.k φ K A W H
15 1 hdmap1ffval K A HDMap1 K = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
16 15 fveq1d K A HDMap1 K W = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h W
17 13 16 syl5eq K A I = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h W
18 fveq2 w = W DVecH K w = DVecH K W
19 fveq2 w = W LCDual K w = LCDual K W
20 fveq2 w = W mapd K w = mapd K W
21 20 sbceq1d w = W [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
22 21 sbcbidv w = W [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
23 22 sbcbidv w = W [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
24 19 23 sbceqbid w = W [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
25 24 sbcbidv w = W [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ LSpan u / n]˙ [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
26 25 sbcbidv w = W [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
27 18 26 sbceqbid w = W [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h [˙ DVecH K W / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
28 fvex DVecH K W V
29 fvex Base u V
30 fvex LSpan u V
31 2 eqeq2i u = U u = DVecH K W
32 31 biimpri u = DVecH K W u = U
33 32 3ad2ant1 u = DVecH K W v = Base u n = LSpan u u = U
34 simp2 u = DVecH K W v = Base u n = LSpan u v = Base u
35 32 fveq2d u = DVecH K W Base u = Base U
36 35 3ad2ant1 u = DVecH K W v = Base u n = LSpan u Base u = Base U
37 34 36 eqtrd u = DVecH K W v = Base u n = LSpan u v = Base U
38 37 3 eqtr4di u = DVecH K W v = Base u n = LSpan u v = V
39 simp3 u = DVecH K W v = Base u n = LSpan u n = LSpan u
40 33 fveq2d u = DVecH K W v = Base u n = LSpan u LSpan u = LSpan U
41 39 40 eqtrd u = DVecH K W v = Base u n = LSpan u n = LSpan U
42 41 6 eqtr4di u = DVecH K W v = Base u n = LSpan u n = N
43 fvex LCDual K W V
44 fvex Base c V
45 fvex LSpan c V
46 id c = LCDual K W c = LCDual K W
47 46 7 eqtr4di c = LCDual K W c = C
48 47 3ad2ant1 c = LCDual K W d = Base c j = LSpan c c = C
49 simp2 c = LCDual K W d = Base c j = LSpan c d = Base c
50 48 fveq2d c = LCDual K W d = Base c j = LSpan c Base c = Base C
51 50 8 eqtr4di c = LCDual K W d = Base c j = LSpan c Base c = D
52 49 51 eqtrd c = LCDual K W d = Base c j = LSpan c d = D
53 simp3 c = LCDual K W d = Base c j = LSpan c j = LSpan c
54 48 fveq2d c = LCDual K W d = Base c j = LSpan c LSpan c = LSpan C
55 54 11 eqtr4di c = LCDual K W d = Base c j = LSpan c LSpan c = J
56 53 55 eqtrd c = LCDual K W d = Base c j = LSpan c j = J
57 fvex mapd K W V
58 id m = mapd K W m = mapd K W
59 58 12 eqtr4di m = mapd K W m = M
60 fveq1 m = M m n 2 nd x = M n 2 nd x
61 60 eqeq1d m = M m n 2 nd x = j h M n 2 nd x = j h
62 fveq1 m = M m n 1 st 1 st x - u 2 nd x = M n 1 st 1 st x - u 2 nd x
63 62 eqeq1d m = M m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
64 61 63 anbi12d m = M m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
65 64 riotabidv m = M ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
66 65 ifeq2d m = M if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
67 66 mpteq2dv m = M x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = x v × d × v if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
68 67 eleq2d m = M a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x v × d × v if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
69 59 68 syl m = mapd K W a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x v × d × v if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
70 57 69 sbcie [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x v × d × v if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
71 simp2 c = C d = D j = J d = D
72 xpeq2 d = D v × d = v × D
73 72 xpeq1d d = D v × d × v = v × D × v
74 71 73 syl c = C d = D j = J v × d × v = v × D × v
75 simp1 c = C d = D j = J c = C
76 75 fveq2d c = C d = D j = J 0 c = 0 C
77 76 10 eqtr4di c = C d = D j = J 0 c = Q
78 simp3 c = C d = D j = J j = J
79 78 fveq1d c = C d = D j = J j h = J h
80 79 eqeq2d c = C d = D j = J M n 2 nd x = j h M n 2 nd x = J h
81 75 fveq2d c = C d = D j = J - c = - C
82 81 9 eqtr4di c = C d = D j = J - c = R
83 82 oveqd c = C d = D j = J 2 nd 1 st x - c h = 2 nd 1 st x R h
84 83 sneqd c = C d = D j = J 2 nd 1 st x - c h = 2 nd 1 st x R h
85 78 84 fveq12d c = C d = D j = J j 2 nd 1 st x - c h = J 2 nd 1 st x R h
86 85 eqeq2d c = C d = D j = J M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
87 80 86 anbi12d c = C d = D j = J M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
88 71 87 riotaeqbidv c = C d = D j = J ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
89 77 88 ifeq12d c = C d = D j = J if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
90 74 89 mpteq12dv c = C d = D j = J x v × d × v if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = x v × D × v if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
91 90 eleq2d c = C d = D j = J a x v × d × v if 2 nd x = 0 u 0 c ι h d | M n 2 nd x = j h M n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x v × D × v if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
92 70 91 syl5bb c = C d = D j = J [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x v × D × v if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
93 48 52 56 92 syl3anc c = LCDual K W d = Base c j = LSpan c [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x v × D × v if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
94 43 44 45 93 sbc3ie [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x v × D × v if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h
95 simp2 u = U v = V n = N v = V
96 95 xpeq1d u = U v = V n = N v × D = V × D
97 96 95 xpeq12d u = U v = V n = N v × D × v = V × D × V
98 simp1 u = U v = V n = N u = U
99 98 fveq2d u = U v = V n = N 0 u = 0 U
100 99 5 eqtr4di u = U v = V n = N 0 u = 0 ˙
101 100 eqeq2d u = U v = V n = N 2 nd x = 0 u 2 nd x = 0 ˙
102 simp3 u = U v = V n = N n = N
103 102 fveq1d u = U v = V n = N n 2 nd x = N 2 nd x
104 103 fveqeq2d u = U v = V n = N M n 2 nd x = J h M N 2 nd x = J h
105 98 fveq2d u = U v = V n = N - u = - U
106 105 4 eqtr4di u = U v = V n = N - u = - ˙
107 106 oveqd u = U v = V n = N 1 st 1 st x - u 2 nd x = 1 st 1 st x - ˙ 2 nd x
108 107 sneqd u = U v = V n = N 1 st 1 st x - u 2 nd x = 1 st 1 st x - ˙ 2 nd x
109 102 108 fveq12d u = U v = V n = N n 1 st 1 st x - u 2 nd x = N 1 st 1 st x - ˙ 2 nd x
110 109 fveqeq2d u = U v = V n = N M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h M N 1 st 1 st x - ˙ 2 nd x = J 2 nd 1 st x R h
111 104 110 anbi12d u = U v = V n = N M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h 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
112 111 riotabidv u = U v = V n = N ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h = ι 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
113 101 112 ifbieq2d u = U v = V n = N if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h = 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
114 97 113 mpteq12dv u = U v = V n = N x v × D × v if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h = x V × D × 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
115 114 eleq2d u = U v = V n = N a x v × D × v if 2 nd x = 0 u Q ι h D | M n 2 nd x = J h M n 1 st 1 st x - u 2 nd x = J 2 nd 1 st x R h a x V × D × 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
116 94 115 syl5bb u = U v = V n = N [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x V × D × 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
117 33 38 42 116 syl3anc u = DVecH K W v = Base u n = LSpan u [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x V × D × 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
118 28 29 30 117 sbc3ie [˙ DVecH K W / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K W / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K W / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x V × D × 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
119 27 118 bitrdi w = W [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h a x V × D × 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
120 119 abbi1dv w = W a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = x V × D × 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
121 eqid w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h = w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h
122 3 fvexi V V
123 8 fvexi D V
124 122 123 xpex V × D V
125 124 122 xpex V × D × V V
126 125 mptex x V × D × 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 V
127 120 121 126 fvmpt W H w H a | [˙ DVecH K w / u]˙ [˙Base u / v]˙ [˙ LSpan u / n]˙ [˙ LCDual K w / c]˙ [˙Base c / d]˙ [˙ LSpan c / j]˙ [˙ mapd K w / m]˙ a x v × d × v if 2 nd x = 0 u 0 c ι h d | m n 2 nd x = j h m n 1 st 1 st x - u 2 nd x = j 2 nd 1 st x - c h W = x V × D × 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
128 17 127 sylan9eq K A W H I = x V × D × 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
129 14 128 syl φ I = x V × D × 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