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↾BaseKI↾LTrn⁡K⁡W
hdmapfval.u ⊢U=DVecH⁡K⁡W
hdmapfval.v ⊢V=BaseU
hdmapfval.n ⊢N=LSpan⁡U
hdmapfval.c ⊢C=LCDual⁡K⁡W
hdmapfval.d ⊢D=BaseC
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⁡zI⁡EJ⁡Ezt

Proof

Step Hyp Ref Expression
1 hdmapval.h ⊢H=LHyp⁡K
2 hdmapfval.e ⊢E=I↾BaseKI↾LTrn⁡K⁡W
3 hdmapfval.u ⊢U=DVecH⁡K⁡W
4 hdmapfval.v ⊢V=BaseU
5 hdmapfval.n ⊢N=LSpan⁡U
6 hdmapfval.c ⊢C=LCDual⁡K⁡W
7 hdmapfval.d ⊢D=BaseC
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↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt
13 12 fveq1d ⊢K∈A→HDMap⁡K⁡W=w∈H⟼a|[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt⁡W
14 10 13 eqtrid ⊢K∈A→S=w∈H⟼a|[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt⁡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↾BaseKI↾LTrn⁡K⁡w=I↾BaseKI↾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→BaseLCDual⁡K⁡w=BaseLCDual⁡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→eHVMap⁡K⁡w⁡ez=eHVMap⁡K⁡W⁡ez
24 23 fveq2d ⊢w=W→i⁡eHVMap⁡K⁡w⁡ez=i⁡eHVMap⁡K⁡W⁡ez
25 24 oteq2d ⊢w=W→zi⁡eHVMap⁡K⁡w⁡ezt=zi⁡eHVMap⁡K⁡W⁡ezt
26 25 fveq2d ⊢w=W→i⁡zi⁡eHVMap⁡K⁡w⁡ezt=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
27 26 eqeq2d ⊢w=W→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
28 27 imbi2d ⊢w=W→¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
29 28 ralbidv ⊢w=W→∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
30 20 29 riotaeqbidv ⊢w=W→ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt=ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
31 30 mpteq2dv ⊢w=W→t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt=t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
32 31 eleq2d ⊢w=W→a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
33 19 32 sbceqbid ⊢w=W→[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
34 33 sbcbidv ⊢w=W→[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔[˙Baseu/v]˙[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
35 18 34 sbceqbid ⊢w=W→[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔[˙DVecH⁡K⁡W/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
36 17 35 sbceqbid ⊢w=W→[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔[˙I↾BaseKI↾LTrn⁡K⁡W/e]˙[˙DVecH⁡K⁡W/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt
37 opex ⊢I↾BaseKI↾LTrn⁡K⁡W∈V
38 fvex ⊢DVecH⁡K⁡W∈V
39 fvex ⊢Baseu∈V
40 simp1 ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→e=I↾BaseKI↾LTrn⁡K⁡W
41 40 2 eqtr4di ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→e=E
42 simp2 ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→u=DVecH⁡K⁡W
43 42 3 eqtr4di ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→u=U
44 simp3 ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→v=Baseu
45 43 fveq2d ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→Baseu=BaseU
46 44 45 eqtrd ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→v=BaseU
47 46 4 eqtr4di ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→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⁡zi⁡eHVMap⁡K⁡W⁡ezt=I⁡zi⁡eHVMap⁡K⁡W⁡ezt
52 fveq1 ⊢i=I→i⁡eHVMap⁡K⁡W⁡ez=I⁡eHVMap⁡K⁡W⁡ez
53 52 oteq2d ⊢i=I→zi⁡eHVMap⁡K⁡W⁡ezt=zI⁡eHVMap⁡K⁡W⁡ezt
54 53 fveq2d ⊢i=I→I⁡zi⁡eHVMap⁡K⁡W⁡ezt=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
55 51 54 eqtrd ⊢i=I→i⁡zi⁡eHVMap⁡K⁡W⁡ezt=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
56 55 eqeq2d ⊢i=I→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
57 56 imbi2d ⊢i=I→¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
58 57 ralbidv ⊢i=I→∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
59 58 riotabidv ⊢i=I→ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt=ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
60 59 mpteq2dv ⊢i=I→t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt=t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
61 60 eleq2d ⊢i=I→a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
62 50 61 syl ⊢i=HDMap1⁡K⁡W→a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
63 48 62 sbcie ⊢[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt
64 simp3 ⊢e=E∧u=U∧v=V→v=V
65 6 fveq2i ⊢BaseC=BaseLCDual⁡K⁡W
66 7 65 eqtr2i ⊢BaseLCDual⁡K⁡W=D
67 66 a1i ⊢e=E∧u=U∧v=V→BaseLCDual⁡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→eHVMap⁡K⁡W⁡ez=EHVMap⁡K⁡W⁡ez
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→EHVMap⁡K⁡W⁡ez=EJ⁡Ez
83 78 82 eqtrd ⊢e=E∧u=U∧v=V→eHVMap⁡K⁡W⁡ez=EJ⁡Ez
84 83 fveq2d ⊢e=E∧u=U∧v=V→I⁡eHVMap⁡K⁡W⁡ez=I⁡EJ⁡Ez
85 84 oteq2d ⊢e=E∧u=U∧v=V→zI⁡eHVMap⁡K⁡W⁡ezt=zI⁡EJ⁡Ezt
86 85 fveq2d ⊢e=E∧u=U∧v=V→I⁡zI⁡eHVMap⁡K⁡W⁡ezt=I⁡zI⁡EJ⁡Ezt
87 86 eqeq2d ⊢e=E∧u=U∧v=V→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt↔y=I⁡zI⁡EJ⁡Ezt
88 77 87 imbi12d ⊢e=E∧u=U∧v=V→¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt↔¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
89 64 88 raleqbidv ⊢e=E∧u=U∧v=V→∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt↔∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
90 67 89 riotaeqbidv ⊢e=E∧u=U∧v=V→ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt=ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
91 64 90 mpteq12dv ⊢e=E∧u=U∧v=V→t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt=t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
92 91 eleq2d ⊢e=E∧u=U∧v=V→a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=I⁡zI⁡eHVMap⁡K⁡W⁡ezt↔a∈t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
93 63 92 bitrid ⊢e=E∧u=U∧v=V→[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔a∈t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
94 41 43 47 93 syl3anc ⊢e=I↾BaseKI↾LTrn⁡K⁡W∧u=DVecH⁡K⁡W∧v=Baseu→[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔a∈t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
95 37 38 39 94 sbc3ie ⊢[˙I↾BaseKI↾LTrn⁡K⁡W/e]˙[˙DVecH⁡K⁡W/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡W/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡W|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡W⁡ezt↔a∈t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
96 36 95 bitrdi ⊢w=W→[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt↔a∈t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
97 96 eqabcdv ⊢w=W→a|[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt=t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
98 eqid ⊢w∈H⟼a|[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt=w∈H⟼a|[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt
99 97 98 4 mptfvmpt ⊢W∈H→w∈H⟼a|[˙I↾BaseKI↾LTrn⁡K⁡w/e]˙[˙DVecH⁡K⁡w/u]˙[˙Baseu/v]˙[˙HDMap1⁡K⁡w/i]˙a∈t∈v⟼ιy∈BaseLCDual⁡K⁡w|∀z∈v¬z∈LSpan⁡u⁡e∪LSpan⁡u⁡t→y=i⁡zi⁡eHVMap⁡K⁡w⁡ezt⁡W=t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
100 14 99 sylan9eq ⊢K∈A∧W∈H→S=t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt
101 11 100 syl ⊢φ→S=t∈V⟼ιy∈D|∀z∈V¬z∈N⁡E∪N⁡t→y=I⁡zI⁡EJ⁡Ezt