Step | Hyp | Ref
| Expression |
1 | | tgrpset.g |
. 2
⊢ 𝐺 = ((TGrp‘𝐾)‘𝑊) |
2 | | tgrpset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
3 | 2 | tgrpfset 35050 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (TGrp‘𝐾) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})) |
4 | 3 | fveq1d 6105 |
. . 3
⊢ (𝐾 ∈ 𝑉 → ((TGrp‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})‘𝑊)) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
6 | 5 | opeq2d 4347 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉 =
〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉) |
7 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔)) |
8 | 5, 5, 7 | mpt2eq123dv 6615 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))) |
9 | 8 | opeq2d 4347 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉) |
10 | 6, 9 | preq12d 4220 |
. . . . 5
⊢ (𝑤 = 𝑊 → {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉} = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉}) |
11 | | eqid 2610 |
. . . . 5
⊢ (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉}) = (𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉}) |
12 | | prex 4836 |
. . . . 5
⊢
{〈(Base‘ndx), ((LTrn‘𝐾)‘𝑊)〉, 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉} ∈ V |
13 | 10, 11, 12 | fvmpt 6191 |
. . . 4
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})‘𝑊) = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉}) |
14 | | tgrpset.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
15 | 14 | opeq2i 4344 |
. . . . 5
⊢
〈(Base‘ndx), 𝑇〉 = 〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉 |
16 | | eqid 2610 |
. . . . . . 7
⊢ (𝑓 ∘ 𝑔) = (𝑓 ∘ 𝑔) |
17 | 14, 14, 16 | mpt2eq123i 6616 |
. . . . . 6
⊢ (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔)) |
18 | 17 | opeq2i 4344 |
. . . . 5
⊢
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉 = 〈(+g‘ndx),
(𝑓 ∈
((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉 |
19 | 15, 18 | preq12i 4217 |
. . . 4
⊢
{〈(Base‘ndx), 𝑇〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉} = {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑊)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑊), 𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ↦ (𝑓 ∘ 𝑔))〉} |
20 | 13, 19 | syl6eqr 2662 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {〈(Base‘ndx),
((LTrn‘𝐾)‘𝑤)〉,
〈(+g‘ndx), (𝑓 ∈ ((LTrn‘𝐾)‘𝑤), 𝑔 ∈ ((LTrn‘𝐾)‘𝑤) ↦ (𝑓 ∘ 𝑔))〉})‘𝑊) = {〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉}) |
21 | 4, 20 | sylan9eq 2664 |
. 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → ((TGrp‘𝐾)‘𝑊) = {〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉}) |
22 | 1, 21 | syl5eq 2656 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐺 = {〈(Base‘ndx), 𝑇〉,
〈(+g‘ndx), (𝑓 ∈ 𝑇, 𝑔 ∈ 𝑇 ↦ (𝑓 ∘ 𝑔))〉}) |