Step | Hyp | Ref
| Expression |
1 | | hdmapfval.k |
. 2
⊢ (𝜑 → (𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻)) |
2 | | hdmapfval.s |
. . . 4
⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) |
3 | | hdmapval.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 3 | hdmapffval 36136 |
. . . . 5
⊢ (𝐾 ∈ 𝐴 → (HDMap‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})) |
5 | 4 | fveq1d 6105 |
. . . 4
⊢ (𝐾 ∈ 𝐴 → ((HDMap‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})‘𝑊)) |
6 | 2, 5 | syl5eq 2656 |
. . 3
⊢ (𝐾 ∈ 𝐴 → 𝑆 = ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})‘𝑊)) |
7 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
8 | 7 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ( I ↾ ((LTrn‘𝐾)‘𝑤)) = ( I ↾ ((LTrn‘𝐾)‘𝑊))) |
9 | 8 | opeq2d 4347 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 〈( I ↾ (Base‘𝐾)), ( I ↾
((LTrn‘𝐾)‘𝑤))〉 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉) |
10 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊)) |
11 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ((HDMap1‘𝐾)‘𝑤) = ((HDMap1‘𝐾)‘𝑊)) |
12 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑊 → ((LCDual‘𝐾)‘𝑤) = ((LCDual‘𝐾)‘𝑊)) |
13 | 12 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → (Base‘((LCDual‘𝐾)‘𝑤)) = (Base‘((LCDual‘𝐾)‘𝑊))) |
14 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑊 → ((HVMap‘𝐾)‘𝑤) = ((HVMap‘𝐾)‘𝑊)) |
15 | 14 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑊 → (((HVMap‘𝐾)‘𝑤)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝑒)) |
16 | 15 | oteq2d 4353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑊 → 〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉 = 〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) |
17 | 16 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑊 → (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉) = (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉)) |
18 | 17 | oteq2d 4353 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑊 → 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉 = 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) |
19 | 18 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑊 → (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉) = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑊 → (𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉) ↔ 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) |
21 | 20 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑊 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
22 | 21 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
23 | 13, 22 | riotaeqbidv 6514 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
24 | 23 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))))) |
25 | 24 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
26 | 11, 25 | sbceqbid 3409 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ([((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔
[((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
27 | 26 | sbcbidv 3457 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ([(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
28 | 10, 27 | sbceqbid 3409 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ([((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ [((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
29 | 9, 28 | sbceqbid 3409 |
. . . . . 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‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
30 | | opex 4859 |
. . . . . . 7
⊢ 〈( I
↾ (Base‘𝐾)), (
I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ V |
31 | | fvex 6113 |
. . . . . . 7
⊢
((DVecH‘𝐾)‘𝑊) ∈ V |
32 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑢)
∈ V |
33 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 〈( I ↾ (Base‘𝐾)), ( I ↾
((LTrn‘𝐾)‘𝑊))〉) |
34 | | hdmapfval.e |
. . . . . . . . 9
⊢ 𝐸 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 |
35 | 33, 34 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑒 = 𝐸) |
36 | | simp2 1055 |
. . . . . . . . 9
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = ((DVecH‘𝐾)‘𝑊)) |
37 | | hdmapfval.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
38 | 36, 37 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑢 = 𝑈) |
39 | | simp3 1056 |
. . . . . . . . . 10
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑢)) |
40 | 38 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → (Base‘𝑢) = (Base‘𝑈)) |
41 | 39, 40 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = (Base‘𝑈)) |
42 | | hdmapfval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑈) |
43 | 41, 42 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → 𝑣 = 𝑉) |
44 | | fvex 6113 |
. . . . . . . . . 10
⊢
((HDMap1‘𝐾)‘𝑊) ∈ V |
45 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = ((HDMap1‘𝐾)‘𝑊)) |
46 | | hdmapfval.i |
. . . . . . . . . . . 12
⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊) |
47 | 45, 46 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → 𝑖 = 𝐼) |
48 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝐼 → (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
49 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝐼 → (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) = (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉)) |
50 | 49 | oteq2d 4353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝐼 → 〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉 = 〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) |
51 | 50 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝐼 → (𝐼‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
52 | 48, 51 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝐼 → (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) |
53 | 52 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝐼 → (𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) ↔ 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) |
54 | 53 | imbi2d 329 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝐼 → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
55 | 54 | ralbidv 2969 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝐼 → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ ∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
56 | 55 | riotabidv 6513 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝐼 → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) = (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) |
57 | 56 | mpteq2dv 4673 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) = (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))))) |
58 | 57 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
59 | 47, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝑖 = ((HDMap1‘𝐾)‘𝑊) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))))) |
60 | 44, 59 | sbcie 3437 |
. . . . . . . . 9
⊢
([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))))) |
61 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑣 = 𝑉) |
62 | | hdmapfval.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (Base‘𝐶) |
63 | | hdmapfval.c |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) |
64 | 63 | fveq2i 6106 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐶) =
(Base‘((LCDual‘𝐾)‘𝑊)) |
65 | 62, 64 | eqtr2i 2633 |
. . . . . . . . . . . . 13
⊢
(Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷 |
66 | 65 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (Base‘((LCDual‘𝐾)‘𝑊)) = 𝐷) |
67 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑢 = 𝑈) |
68 | 67 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = (LSpan‘𝑈)) |
69 | | hdmapfval.n |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑁 = (LSpan‘𝑈) |
70 | 68, 69 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (LSpan‘𝑢) = 𝑁) |
71 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 𝑒 = 𝐸) |
72 | 71 | sneqd 4137 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → {𝑒} = {𝐸}) |
73 | 70, 72 | fveq12d 6109 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑒}) = (𝑁‘{𝐸})) |
74 | 70 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((LSpan‘𝑢)‘{𝑡}) = (𝑁‘{𝑡})) |
75 | 73, 74 | uneq12d 3730 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) = ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡}))) |
76 | 75 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))) |
77 | 76 | notbid 307 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) ↔ ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})))) |
78 | 71 | oteq1d 4352 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉 = 〈𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) |
79 | 71 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (((HVMap‘𝐾)‘𝑊)‘𝐸)) |
80 | | hdmapfval.j |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊) |
81 | 80 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽‘𝐸) = (((HVMap‘𝐾)‘𝑊)‘𝐸) |
82 | 79, 81 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (((HVMap‘𝐾)‘𝑊)‘𝑒) = (𝐽‘𝐸)) |
83 | 82 | oteq2d 4353 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝐸, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉 = 〈𝐸, (𝐽‘𝐸), 𝑧〉) |
84 | 78, 83 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉 = 〈𝐸, (𝐽‘𝐸), 𝑧〉) |
85 | 84 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉) = (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉)) |
86 | 85 | oteq2d 4353 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → 〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉 = 〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉) |
87 | 86 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)) |
88 | 87 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉) ↔ 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))) |
89 | 77, 88 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ((¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))) |
90 | 61, 89 | raleqbidv 3129 |
. . . . . . . . . . . 12
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)) ↔ ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))) |
91 | 66, 90 | riotaeqbidv 6514 |
. . . . . . . . . . 11
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉))) = (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))) |
92 | 61, 91 | mpteq12dv 4663 |
. . . . . . . . . 10
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
93 | 92 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → (𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
94 | 60, 93 | syl5bb 271 |
. . . . . . . 8
⊢ ((𝑒 = 𝐸 ∧ 𝑢 = 𝑈 ∧ 𝑣 = 𝑉) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
95 | 35, 38, 43, 94 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝑒 = 〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑊))〉 ∧ 𝑢 = ((DVecH‘𝐾)‘𝑊) ∧ 𝑣 = (Base‘𝑢)) → ([((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
96 | 30, 31, 32, 95 | sbc3ie 3474 |
. . . . . 6
⊢
([〈( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 / 𝑒][((DVecH‘𝐾)‘𝑊) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑊) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑊))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑊)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
97 | 29, 96 | syl6bb 275 |
. . . . 5
⊢ (𝑤 = 𝑊 → ([〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉)))) ↔ 𝑎 ∈ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))))) |
98 | 97 | abbi1dv 2730 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))} = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
99 | | eqid 2610 |
. . . 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‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))}) |
100 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑈)
∈ V |
101 | 42, 100 | eqeltri 2684 |
. . . . 5
⊢ 𝑉 ∈ V |
102 | 101 | mptex 6390 |
. . . 4
⊢ (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉)))) ∈ V |
103 | 98, 99, 102 | fvmpt 6191 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑎 ∣ [〈( I ↾
(Base‘𝐾)), ( I
↾ ((LTrn‘𝐾)‘𝑤))〉 / 𝑒][((DVecH‘𝐾)‘𝑤) / 𝑢][(Base‘𝑢) / 𝑣][((HDMap1‘𝐾)‘𝑤) / 𝑖]𝑎 ∈ (𝑡 ∈ 𝑣 ↦ (℩𝑦 ∈ (Base‘((LCDual‘𝐾)‘𝑤))∀𝑧 ∈ 𝑣 (¬ 𝑧 ∈ (((LSpan‘𝑢)‘{𝑒}) ∪ ((LSpan‘𝑢)‘{𝑡})) → 𝑦 = (𝑖‘〈𝑧, (𝑖‘〈𝑒, (((HVMap‘𝐾)‘𝑤)‘𝑒), 𝑧〉), 𝑡〉))))})‘𝑊) = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
104 | 6, 103 | sylan9eq 2664 |
. 2
⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |
105 | 1, 104 | syl 17 |
1
⊢ (𝜑 → 𝑆 = (𝑡 ∈ 𝑉 ↦ (℩𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝑉 (¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑡})) → 𝑦 = (𝐼‘〈𝑧, (𝐼‘〈𝐸, (𝐽‘𝐸), 𝑧〉), 𝑡〉))))) |