| Step | Hyp | Ref
| Expression |
| 1 | | hdmapfval.k |
. 2
⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) |
| 2 | | hdmapfval.s |
. . . 4
⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
| 3 | | hdmapval.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | 3 | hdmapffval 41828 |
. . . . 5
⊢ (𝐾 ∈ 𝐴 → (HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})) |
| 5 | 4 | fveq1d 6908 |
. . . 4
⊢ (𝐾 ∈ 𝐴 → ((HDMap‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})‘𝑊)) |
| 6 | 2, 5 | eqtrid 2789 |
. . 3
⊢ (𝐾 ∈ 𝐴 → 𝑆 = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})‘𝑊)) |
| 7 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
| 8 | 7 | reseq2d 5997 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ( I ↾ ((LTrn‘𝐾)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑊))) |
| 9 | 8 | opeq2d 4880 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 〈( I ↾ (Base‘𝐾)), ( I ↾
((LTrn‘𝐾)‘𝑤))〉 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉) |
| 10 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊)) |
| 11 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ((HDMap1‘𝐾)‘𝑤) = ((HDMap1‘𝐾)‘𝑊)) |
| 12 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → (Base‘((LCDual‘𝐾)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑊))) |
| 13 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑊 → ((HVMap‘𝐾)‘𝑤) = ((HVMap‘𝐾)‘𝑊)) |
| 14 | 13 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑊 → (((HVMap‘𝐾)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝑒)) |
| 15 | 14 | oteq2d 4886 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑊 → 〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉 = 〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) |
| 16 | 15 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑊 → (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉) = (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉)) |
| 17 | 16 | oteq2d 4886 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉 = 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) |
| 18 | 17 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉) = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
| 19 | 18 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑊 → (𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉) ↔ 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) |
| 20 | 19 | imbi2d 340 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑊 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 21 | 20 | ralbidv 3178 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 22 | 12, 21 | riotaeqbidv 7391 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 23 | 22 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))))) |
| 24 | 23 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 25 | 11, 24 | sbceqbid 3795 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ([((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔
[((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 26 | 25 | sbcbidv 3845 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 27 | 10, 26 | sbceqbid 3795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 28 | 9, 27 | sbceqbid 3795 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ([〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 29 | | opex 5469 |
. . . . . . 7
⊢ 〈( I
↾ (Base‘𝐾)), (
I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ V |
| 30 | | fvex 6919 |
. . . . . . 7
⊢
((DVecH‘𝐾)‘𝑊) ∈ V |
| 31 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝑢)
∈ V |
| 32 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 〈( I ↾ (Base‘𝐾)), ( I ↾
((LTrn‘𝐾)‘𝑊))〉) |
| 33 | | hdmapfval.e |
. . . . . . . . 9
⊢ 𝐸 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 |
| 34 | 32, 33 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 𝐸) |
| 35 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = ((DVecH‘𝐾)‘𝑊)) |
| 36 | | hdmapfval.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 37 | 35, 36 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = 𝑈) |
| 38 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑢)) |
| 39 | 37 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → (Base‘𝑢) = (Base‘𝑈)) |
| 40 | 38, 39 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑈)) |
| 41 | | hdmapfval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑈) |
| 42 | 40, 41 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = 𝑉) |
| 43 | | fvex 6919 |
. . . . . . . . . 10
⊢
((HDMap1‘𝐾)‘𝑊) ∈ V |
| 44 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = ((HDMap1‘𝐾)‘𝑊)) |
| 45 | | hdmapfval.i |
. . . . . . . . . . . 12
⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) |
| 46 | 44, 45 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = 𝐼) |
| 47 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝐼 → (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
| 48 | | fveq1 6905 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝐼 → (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) = (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉)) |
| 49 | 48 | oteq2d 4886 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝐼 → 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉 = 〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) |
| 50 | 49 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝐼 → (𝐼‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
| 51 | 47, 50 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝐼 → (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
| 52 | 51 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝐼 → (𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) ↔ 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) |
| 53 | 52 | imbi2d 340 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐼 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 54 | 53 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝐼 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 55 | 54 | riotabidv 7390 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
| 56 | 55 | mpteq2dv 5244 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))))) |
| 57 | 56 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 58 | 46, 57 | syl 17 |
. . . . . . . . . 10
⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
| 59 | 43, 58 | sbcie 3830 |
. . . . . . . . 9
⊢
([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))))) |
| 60 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉) |
| 61 | | hdmapfval.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (Base‘𝐶) |
| 62 | | hdmapfval.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
| 63 | 62 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐶) =
(Base‘((LCDual‘𝐾)‘𝑊)) |
| 64 | 61, 63 | eqtr2i 2766 |
. . . . . . . . . . . . 13
⊢
(Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷 |
| 65 | 64 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷) |
| 66 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑢 = 𝑈) |
| 67 | 66 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = (LSpan‘𝑈)) |
| 68 | | hdmapfval.n |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑁 = (LSpan‘𝑈) |
| 69 | 67, 68 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = 𝑁) |
| 70 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑒 = 𝐸) |
| 71 | 70 | sneqd 4638 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → {𝑒} = {𝐸}) |
| 72 | 69, 71 | fveq12d 6913 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑒}) = (𝑁‘{𝐸})) |
| 73 | 69 | fveq1d 6908 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑡}) = (𝑁‘{𝑡})) |
| 74 | 72, 73 | uneq12d 4169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) = ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))) |
| 75 | 74 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))) |
| 76 | 75 | notbid 318 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))) |
| 77 | 70 | oteq1d 4885 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉 = 〈𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) |
| 78 | 70 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝐸)) |
| 79 | | hdmapfval.j |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) |
| 80 | 79 | fveq1i 6907 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽‘𝐸) = (((HVMap‘𝐾)‘𝑊)‘𝐸) |
| 81 | 78, 80 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (𝐽‘𝐸)) |
| 82 | 81 | oteq2d 4886 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉 = 〈𝐸, (𝐽‘𝐸), 𝑧〉) |
| 83 | 77, 82 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉 = 〈𝐸, (𝐽‘𝐸), 𝑧〉) |
| 84 | 83 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) = (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉)) |
| 85 | 84 | oteq2d 4886 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉 = 〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉) |
| 86 | 85 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)) |
| 87 | 86 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) ↔ 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))) |
| 88 | 76, 87 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))) |
| 89 | 60, 88 | raleqbidv 3346 |
. . . . . . . . . . . 12
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))) |
| 90 | 65, 89 | riotaeqbidv 7391 |
. . . . . . . . . . 11
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) = (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))) |
| 91 | 60, 90 | mpteq12dv 5233 |
. . . . . . . . . 10
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
| 92 | 91 | eleq2d 2827 |
. . . . . . . . 9
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
| 93 | 59, 92 | bitrid 283 |
. . . . . . . 8
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
| 94 | 34, 37, 42, 93 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
| 95 | 29, 30, 31, 94 | sbc3ie 3868 |
. . . . . 6
⊢
([〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
| 96 | 28, 95 | bitrdi 287 |
. . . . 5
⊢ (𝑤 = 𝑊 → ([〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
| 97 | 96 | eqabcdv 2876 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))} = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
| 98 | | eqid 2737 |
. . . 4
⊢ (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))}) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))}) |
| 99 | 97, 98, 41 | mptfvmpt 7248 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})‘𝑊) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
| 100 | 6, 99 | sylan9eq 2797 |
. 2
⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
| 101 | 1, 100 | syl 17 |
1
⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |