Metamath Proof Explorer

Theorem hdmapfval

Description: Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015)

Ref Expression
Hypotheses hdmapval.h ⊢ H = LHyp ⁡ K
hdmapfval.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
hdmapfval.u ⊢ U = DVecH ⁡ K ⁡ W
hdmapfval.v ⊢ V = Base U
hdmapfval.n ⊢ N = LSpan ⁡ U
hdmapfval.c ⊢ C = LCDual ⁡ K ⁡ W
hdmapfval.d ⊢ D = Base C
hdmapfval.j ⊢ J = HVMap ⁡ K ⁡ W
hdmapfval.i ⊢ I = HDMap1 ⁡ K ⁡ W
hdmapfval.s ⊢ S = HDMap ⁡ K ⁡ W
hdmapfval.k ⊢ φ → K ∈ A ∧ W ∈ H
Assertion hdmapfval ⊢ φ → S = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t

Proof

Step Hyp Ref Expression
1 hdmapval.h ⊢ H = LHyp ⁡ K
2 hdmapfval.e ⊢ E = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
3 hdmapfval.u ⊢ U = DVecH ⁡ K ⁡ W
4 hdmapfval.v ⊢ V = Base U
5 hdmapfval.n ⊢ N = LSpan ⁡ U
6 hdmapfval.c ⊢ C = LCDual ⁡ K ⁡ W
7 hdmapfval.d ⊢ D = Base C
8 hdmapfval.j ⊢ J = HVMap ⁡ K ⁡ W
9 hdmapfval.i ⊢ I = HDMap1 ⁡ K ⁡ W
10 hdmapfval.s ⊢ S = HDMap ⁡ K ⁡ W
11 hdmapfval.k ⊢ φ → K ∈ A ∧ W ∈ H
12 1 hdmapffval ⊢ K ∈ A → HDMap ⁡ K = w ∈ H ⟼ a | [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t
13 12 fveq1d ⊢ K ∈ A → HDMap ⁡ K ⁡ W = w ∈ H ⟼ a | [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ⁡ W
14 10 13 eqtrid ⊢ K ∈ A → S = w ∈ H ⟼ a | [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ⁡ W
15 fveq2 ⊢ w = W → LTrn ⁡ K ⁡ w = LTrn ⁡ K ⁡ W
16 15 reseq2d ⊢ w = W → I ↾ LTrn ⁡ K ⁡ w = I ↾ LTrn ⁡ K ⁡ W
17 16 opeq2d ⊢ w = W → I ↾ Base K I ↾ LTrn ⁡ K ⁡ w = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
18 fveq2 ⊢ w = W → DVecH ⁡ K ⁡ w = DVecH ⁡ K ⁡ W
19 fveq2 ⊢ w = W → HDMap1 ⁡ K ⁡ w = HDMap1 ⁡ K ⁡ W
20 2fveq3 ⊢ w = W → Base LCDual ⁡ K ⁡ w = Base LCDual ⁡ K ⁡ W
21 fveq2 ⊢ w = W → HVMap ⁡ K ⁡ w = HVMap ⁡ K ⁡ W
22 21 fveq1d ⊢ w = W → HVMap ⁡ K ⁡ w ⁡ e = HVMap ⁡ K ⁡ W ⁡ e
23 22 oteq2d ⊢ w = W → e HVMap ⁡ K ⁡ w ⁡ e z = e HVMap ⁡ K ⁡ W ⁡ e z
24 23 fveq2d ⊢ w = W → i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z = i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z
25 24 oteq2d ⊢ w = W → z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t = z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
26 25 fveq2d ⊢ w = W → i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
27 26 eqeq2d ⊢ w = W → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
28 27 imbi2d ⊢ w = W → ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
29 28 ralbidv ⊢ w = W → ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
30 20 29 riotaeqbidv ⊢ w = W → ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t = ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
31 30 mpteq2dv ⊢ w = W → t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t = t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
32 31 eleq2d ⊢ w = W → a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
33 19 32 sbceqbid ⊢ w = W → [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
34 33 sbcbidv ⊢ w = W → [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
35 18 34 sbceqbid ⊢ w = W → [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ [˙ DVecH ⁡ K ⁡ W / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
36 17 35 sbceqbid ⊢ w = W → [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W / e]˙ [˙ DVecH ⁡ K ⁡ W / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
37 opex ⊢ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∈ V
38 fvex ⊢ DVecH ⁡ K ⁡ W ∈ V
39 fvex ⊢ Base u ∈ V
40 simp1 ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W
41 40 2 eqtr4di ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → e = E
42 simp2 ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → u = DVecH ⁡ K ⁡ W
43 42 3 eqtr4di ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → u = U
44 simp3 ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → v = Base u
45 43 fveq2d ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → Base u = Base U
46 44 45 eqtrd ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → v = Base U
47 46 4 eqtr4di ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → v = V
48 fvex ⊢ HDMap1 ⁡ K ⁡ W ∈ V
49 id ⊢ i = HDMap1 ⁡ K ⁡ W → i = HDMap1 ⁡ K ⁡ W
50 49 9 eqtr4di ⊢ i = HDMap1 ⁡ K ⁡ W → i = I
51 fveq1 ⊢ i = I → i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = I ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
52 fveq1 ⊢ i = I → i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z = I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z
53 52 oteq2d ⊢ i = I → z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
54 53 fveq2d ⊢ i = I → I ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
55 51 54 eqtrd ⊢ i = I → i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
56 55 eqeq2d ⊢ i = I → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
57 56 imbi2d ⊢ i = I → ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
58 57 ralbidv ⊢ i = I → ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
59 58 riotabidv ⊢ i = I → ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
60 59 mpteq2dv ⊢ i = I → t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
61 60 eleq2d ⊢ i = I → a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
62 50 61 syl ⊢ i = HDMap1 ⁡ K ⁡ W → a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
63 48 62 sbcie ⊢ [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t
64 simp3 ⊢ e = E ∧ u = U ∧ v = V → v = V
65 6 fveq2i ⊢ Base C = Base LCDual ⁡ K ⁡ W
66 7 65 eqtr2i ⊢ Base LCDual ⁡ K ⁡ W = D
67 66 a1i ⊢ e = E ∧ u = U ∧ v = V → Base LCDual ⁡ K ⁡ W = D
68 simp2 ⊢ e = E ∧ u = U ∧ v = V → u = U
69 68 fveq2d ⊢ e = E ∧ u = U ∧ v = V → LSpan ⁡ u = LSpan ⁡ U
70 69 5 eqtr4di ⊢ e = E ∧ u = U ∧ v = V → LSpan ⁡ u = N
71 simp1 ⊢ e = E ∧ u = U ∧ v = V → e = E
72 71 sneqd ⊢ e = E ∧ u = U ∧ v = V → e = E
73 70 72 fveq12d ⊢ e = E ∧ u = U ∧ v = V → LSpan ⁡ u ⁡ e = N ⁡ E
74 70 fveq1d ⊢ e = E ∧ u = U ∧ v = V → LSpan ⁡ u ⁡ t = N ⁡ t
75 73 74 uneq12d ⊢ e = E ∧ u = U ∧ v = V → LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t = N ⁡ E ∪ N ⁡ t
76 75 eleq2d ⊢ e = E ∧ u = U ∧ v = V → z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t ↔ z ∈ N ⁡ E ∪ N ⁡ t
77 76 notbid ⊢ e = E ∧ u = U ∧ v = V → ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t ↔ ¬ z ∈ N ⁡ E ∪ N ⁡ t
78 71 oteq1d ⊢ e = E ∧ u = U ∧ v = V → e HVMap ⁡ K ⁡ W ⁡ e z = E HVMap ⁡ K ⁡ W ⁡ e z
79 71 fveq2d ⊢ e = E ∧ u = U ∧ v = V → HVMap ⁡ K ⁡ W ⁡ e = HVMap ⁡ K ⁡ W ⁡ E
80 8 fveq1i ⊢ J ⁡ E = HVMap ⁡ K ⁡ W ⁡ E
81 79 80 eqtr4di ⊢ e = E ∧ u = U ∧ v = V → HVMap ⁡ K ⁡ W ⁡ e = J ⁡ E
82 81 oteq2d ⊢ e = E ∧ u = U ∧ v = V → E HVMap ⁡ K ⁡ W ⁡ e z = E J ⁡ E z
83 78 82 eqtrd ⊢ e = E ∧ u = U ∧ v = V → e HVMap ⁡ K ⁡ W ⁡ e z = E J ⁡ E z
84 83 fveq2d ⊢ e = E ∧ u = U ∧ v = V → I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z = I ⁡ E J ⁡ E z
85 84 oteq2d ⊢ e = E ∧ u = U ∧ v = V → z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = z I ⁡ E J ⁡ E z t
86 85 fveq2d ⊢ e = E ∧ u = U ∧ v = V → I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = I ⁡ z I ⁡ E J ⁡ E z t
87 86 eqeq2d ⊢ e = E ∧ u = U ∧ v = V → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ y = I ⁡ z I ⁡ E J ⁡ E z t
88 77 87 imbi12d ⊢ e = E ∧ u = U ∧ v = V → ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
89 64 88 raleqbidv ⊢ e = E ∧ u = U ∧ v = V → ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
90 67 89 riotaeqbidv ⊢ e = E ∧ u = U ∧ v = V → ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
91 64 90 mpteq12dv ⊢ e = E ∧ u = U ∧ v = V → t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
92 91 eleq2d ⊢ e = E ∧ u = U ∧ v = V → a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = I ⁡ z I ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ a ∈ t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
93 63 92 bitrid ⊢ e = E ∧ u = U ∧ v = V → [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ a ∈ t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
94 41 43 47 93 syl3anc ⊢ e = I ↾ Base K I ↾ LTrn ⁡ K ⁡ W ∧ u = DVecH ⁡ K ⁡ W ∧ v = Base u → [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ a ∈ t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
95 37 38 39 94 sbc3ie ⊢ [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ W / e]˙ [˙ DVecH ⁡ K ⁡ W / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ W / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ W | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ W ⁡ e z t ↔ a ∈ t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
96 36 95 bitrdi ⊢ w = W → [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ↔ a ∈ t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
97 96 eqabcdv ⊢ w = W → a | [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
98 eqid ⊢ w ∈ H ⟼ a | [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t = w ∈ H ⟼ a | [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t
99 97 98 4 mptfvmpt ⊢ W ∈ H → w ∈ H ⟼ a | [˙ I ↾ Base K I ↾ LTrn ⁡ K ⁡ w / e]˙ [˙ DVecH ⁡ K ⁡ w / u]˙ [˙Base u / v]˙ [˙ HDMap1 ⁡ K ⁡ w / i]˙ a ∈ t ∈ v ⟼ ι y ∈ Base LCDual ⁡ K ⁡ w | ∀ z ∈ v ¬ z ∈ LSpan ⁡ u ⁡ e ∪ LSpan ⁡ u ⁡ t → y = i ⁡ z i ⁡ e HVMap ⁡ K ⁡ w ⁡ e z t ⁡ W = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
100 14 99 sylan9eq ⊢ K ∈ A ∧ W ∈ H → S = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t
101 11 100 syl ⊢ φ → S = t ∈ V ⟼ ι y ∈ D | ∀ z ∈ V ¬ z ∈ N ⁡ E ∪ N ⁡ t → y = I ⁡ z I ⁡ E J ⁡ E z t