Step | Hyp | Ref
| Expression |
1 | | ldualset.w |
. 2
⊢ (𝜑 → 𝑊 ∈ 𝑋) |
2 | | elex 3426 |
. 2
⊢ (𝑊 ∈ 𝑋 → 𝑊 ∈ V) |
3 | | ldualset.d |
. . 3
⊢ 𝐷 = (LDual‘𝑊) |
4 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = (LFnl‘𝑊)) |
5 | | ldualset.f |
. . . . . . . 8
⊢ 𝐹 = (LFnl‘𝑊) |
6 | 4, 5 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (LFnl‘𝑤) = 𝐹) |
7 | 6 | opeq2d 4791 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(Base‘ndx),
(LFnl‘𝑤)〉 =
〈(Base‘ndx), 𝐹〉) |
8 | | fveq2 6717 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
9 | | ldualset.r |
. . . . . . . . . . . . 13
⊢ 𝑅 = (Scalar‘𝑊) |
10 | 8, 9 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝑅) |
11 | 10 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 →
(+g‘(Scalar‘𝑤)) = (+g‘𝑅)) |
12 | | ldualset.a |
. . . . . . . . . . 11
⊢ + =
(+g‘𝑅) |
13 | 11, 12 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 →
(+g‘(Scalar‘𝑤)) = + ) |
14 | | ofeq 7471 |
. . . . . . . . . 10
⊢
((+g‘(Scalar‘𝑤)) = + → ∘f
(+g‘(Scalar‘𝑤)) = ∘f + ) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ∘f
(+g‘(Scalar‘𝑤)) = ∘f + ) |
16 | 6 | sqxpeqd 5583 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ((LFnl‘𝑤) × (LFnl‘𝑤)) = (𝐹 × 𝐹)) |
17 | 15, 16 | reseq12d 5852 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ( ∘f
(+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ( ∘f + ↾
(𝐹 × 𝐹))) |
18 | | ldualset.p |
. . . . . . . 8
⊢ ✚ = (
∘f + ↾ (𝐹 × 𝐹)) |
19 | 17, 18 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ( ∘f
(+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤))) = ✚ ) |
20 | 19 | opeq2d 4791 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(+g‘ndx), (
∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))〉 = 〈(+g‘ndx),
✚
〉) |
21 | 10 | fveq2d 6721 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 →
(oppr‘(Scalar‘𝑤)) = (oppr‘𝑅)) |
22 | | ldualset.o |
. . . . . . . 8
⊢ 𝑂 =
(oppr‘𝑅) |
23 | 21, 22 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 →
(oppr‘(Scalar‘𝑤)) = 𝑂) |
24 | 23 | opeq2d 4791 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(Scalar‘ndx),
(oppr‘(Scalar‘𝑤))〉 = 〈(Scalar‘ndx), 𝑂〉) |
25 | 7, 20, 24 | tpeq123d 4664 |
. . . . 5
⊢ (𝑤 = 𝑊 → {〈(Base‘ndx),
(LFnl‘𝑤)〉,
〈(+g‘ndx), ( ∘f
(+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))〉, 〈(Scalar‘ndx),
(oppr‘(Scalar‘𝑤))〉} = {〈(Base‘ndx), 𝐹〉,
〈(+g‘ndx), ✚ 〉,
〈(Scalar‘ndx), 𝑂〉}) |
26 | 10 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = (Base‘𝑅)) |
27 | | ldualset.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝑅) |
28 | 26, 27 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Base‘(Scalar‘𝑤)) = 𝐾) |
29 | 10 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 →
(.r‘(Scalar‘𝑤)) = (.r‘𝑅)) |
30 | | ldualset.t |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑅) |
31 | 29, 30 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 →
(.r‘(Scalar‘𝑤)) = · ) |
32 | | ofeq 7471 |
. . . . . . . . . . 11
⊢
((.r‘(Scalar‘𝑤)) = · →
∘f (.r‘(Scalar‘𝑤)) = ∘f · ) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ∘f
(.r‘(Scalar‘𝑤)) = ∘f · ) |
34 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → 𝑓 = 𝑓) |
35 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
36 | | ldualset.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Base‘𝑊) |
37 | 35, 36 | eqtr4di 2796 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
38 | 37 | xpeq1d 5580 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ((Base‘𝑤) × {𝑘}) = (𝑉 × {𝑘})) |
39 | 33, 34, 38 | oveq123d 7234 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (𝑓 ∘f
(.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})) = (𝑓 ∘f · (𝑉 × {𝑘}))) |
40 | 28, 6, 39 | mpoeq123dv 7286 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f
(.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘})))) |
41 | | ldualset.s |
. . . . . . . 8
⊢ ∙ =
(𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘}))) |
42 | 40, 41 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f
(.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘}))) = ∙ ) |
43 | 42 | opeq2d 4791 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(
·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f
(.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))〉 = 〈(
·𝑠 ‘ndx), ∙
〉) |
44 | 43 | sneqd 4553 |
. . . . 5
⊢ (𝑤 = 𝑊 → {〈(
·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f
(.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))〉} = {〈(
·𝑠 ‘ndx), ∙
〉}) |
45 | 25, 44 | uneq12d 4078 |
. . . 4
⊢ (𝑤 = 𝑊 → ({〈(Base‘ndx),
(LFnl‘𝑤)〉,
〈(+g‘ndx), ( ∘f
(+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))〉, 〈(Scalar‘ndx),
(oppr‘(Scalar‘𝑤))〉} ∪ {〈(
·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f
(.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))〉}) = ({〈(Base‘ndx),
𝐹〉,
〈(+g‘ndx), ✚ 〉,
〈(Scalar‘ndx), 𝑂〉} ∪ {〈(
·𝑠 ‘ndx), ∙
〉})) |
46 | | df-ldual 36875 |
. . . 4
⊢ LDual =
(𝑤 ∈ V ↦
({〈(Base‘ndx), (LFnl‘𝑤)〉, 〈(+g‘ndx), (
∘f (+g‘(Scalar‘𝑤)) ↾ ((LFnl‘𝑤) × (LFnl‘𝑤)))〉, 〈(Scalar‘ndx),
(oppr‘(Scalar‘𝑤))〉} ∪ {〈(
·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑤)), 𝑓 ∈ (LFnl‘𝑤) ↦ (𝑓 ∘f
(.r‘(Scalar‘𝑤))((Base‘𝑤) × {𝑘})))〉})) |
47 | | tpex 7532 |
. . . . 5
⊢
{〈(Base‘ndx), 𝐹〉, 〈(+g‘ndx),
✚
〉, 〈(Scalar‘ndx), 𝑂〉} ∈ V |
48 | | snex 5324 |
. . . . 5
⊢ {〈(
·𝑠 ‘ndx), ∙ 〉} ∈
V |
49 | 47, 48 | unex 7531 |
. . . 4
⊢
({〈(Base‘ndx), 𝐹〉, 〈(+g‘ndx),
✚
〉, 〈(Scalar‘ndx), 𝑂〉} ∪ {〈(
·𝑠 ‘ndx), ∙ 〉}) ∈
V |
50 | 45, 46, 49 | fvmpt 6818 |
. . 3
⊢ (𝑊 ∈ V →
(LDual‘𝑊) =
({〈(Base‘ndx), 𝐹〉, 〈(+g‘ndx),
✚
〉, 〈(Scalar‘ndx), 𝑂〉} ∪ {〈(
·𝑠 ‘ndx), ∙
〉})) |
51 | 3, 50 | syl5eq 2790 |
. 2
⊢ (𝑊 ∈ V → 𝐷 = ({〈(Base‘ndx),
𝐹〉,
〈(+g‘ndx), ✚ 〉,
〈(Scalar‘ndx), 𝑂〉} ∪ {〈(
·𝑠 ‘ndx), ∙
〉})) |
52 | 1, 2, 51 | 3syl 18 |
1
⊢ (𝜑 → 𝐷 = ({〈(Base‘ndx), 𝐹〉,
〈(+g‘ndx), ✚ 〉,
〈(Scalar‘ndx), 𝑂〉} ∪ {〈(
·𝑠 ‘ndx), ∙
〉})) |