Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | fveq2 6191 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | tgrpset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | syl6eqr 2674 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
6 | 5 | fveq1d 6193 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
7 | 6 | opeq2d 4409 |
. . . . 5
⊢ (𝑘 = 𝐾 → 〈(Base‘ndx),
((LTrn‘𝑘)‘𝑤)〉 =
〈(Base‘ndx), ((LTrn‘𝐾)‘𝑤)〉) |
8 | | eqidd 2623 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔)) |
9 | 6, 6, 8 | mpt2eq123dv 6717 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))) |
10 | 9 | opeq2d 4409 |
. . . . 5
⊢ (𝑘 = 𝐾 → 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉) |
11 | 7, 10 | preq12d 4276 |
. . . 4
⊢ (𝑘 = 𝐾 → {〈(Base‘ndx),
((LTrn‘𝑘)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉} = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉}) |
12 | 4, 11 | mpteq12dv 4733 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ {〈(Base‘ndx),
((LTrn‘𝑘)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉}) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) |
13 | | df-tgrp 36031 |
. . 3
⊢ TGrp =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦
{〈(Base‘ndx), ((LTrn‘𝑘)‘𝑤)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝑘)‘𝑤), 𝑔 ∈ ((LTrn‘𝑘)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) |
14 | | fvex 6201 |
. . . . 5
⊢
(LHyp‘𝐾)
∈ V |
15 | 3, 14 | eqeltri 2697 |
. . . 4
⊢ 𝐻 ∈ V |
16 | 15 | mptex 6486 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉}) ∈ V |
17 | 12, 13, 16 | fvmpt 6282 |
. 2
⊢ (𝐾 ∈ V →
(TGrp‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) |
18 | 1, 17 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (TGrp‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) |