Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6839 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | tgrpset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6839 |
. . . . . . 7
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
6 | 5 | fveq1d 6841 |
. . . . . 6
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
7 | 6 | opeq2d 4835 |
. . . . 5
β’ (π = πΎ β β¨(Baseβndx),
((LTrnβπ)βπ€)β© =
β¨(Baseβndx), ((LTrnβπΎ)βπ€)β©) |
8 | | eqidd 2738 |
. . . . . . 7
β’ (π = πΎ β (π β π) = (π β π)) |
9 | 6, 6, 8 | mpoeq123dv 7426 |
. . . . . 6
β’ (π = πΎ β (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π)) = (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))) |
10 | 9 | opeq2d 4835 |
. . . . 5
β’ (π = πΎ β β¨(+gβndx),
(π β
((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β© = β¨(+gβndx),
(π β
((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©) |
11 | 7, 10 | preq12d 4700 |
. . . 4
β’ (π = πΎ β {β¨(Baseβndx),
((LTrnβπ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©} = {β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©}) |
12 | 4, 11 | mpteq12dv 5194 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ {β¨(Baseβndx),
((LTrnβπ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©}) = (π€ β π» β¦ {β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©})) |
13 | | df-tgrp 39144 |
. . 3
β’ TGrp =
(π β V β¦ (π€ β (LHypβπ) β¦
{β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx),
(π β
((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©})) |
14 | 12, 13, 3 | mptfvmpt 7174 |
. 2
β’ (πΎ β V β
(TGrpβπΎ) = (π€ β π» β¦ {β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©})) |
15 | 1, 14 | syl 17 |
1
β’ (πΎ β π β (TGrpβπΎ) = (π€ β π» β¦ {β¨(Baseβndx),
((LTrnβπΎ)βπ€)β©,
β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©})) |