Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6843 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | dibval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (DIsoAβπ) = (DIsoAβπΎ)) |
6 | 5 | fveq1d 6845 |
. . . . . 6
β’ (π = πΎ β ((DIsoAβπ)βπ€) = ((DIsoAβπΎ)βπ€)) |
7 | 6 | dmeqd 5862 |
. . . . 5
β’ (π = πΎ β dom ((DIsoAβπ)βπ€) = dom ((DIsoAβπΎ)βπ€)) |
8 | 6 | fveq1d 6845 |
. . . . . 6
β’ (π = πΎ β (((DIsoAβπ)βπ€)βπ₯) = (((DIsoAβπΎ)βπ€)βπ₯)) |
9 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
10 | 9 | fveq1d 6845 |
. . . . . . . 8
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
11 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
12 | | dibval.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΎ) |
13 | 11, 12 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π = πΎ β (Baseβπ) = π΅) |
14 | 13 | reseq2d 5938 |
. . . . . . . 8
β’ (π = πΎ β ( I βΎ (Baseβπ)) = ( I βΎ π΅)) |
15 | 10, 14 | mpteq12dv 5197 |
. . . . . . 7
β’ (π = πΎ β (π β ((LTrnβπ)βπ€) β¦ ( I βΎ (Baseβπ))) = (π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))) |
16 | 15 | sneqd 4599 |
. . . . . 6
β’ (π = πΎ β {(π β ((LTrnβπ)βπ€) β¦ ( I βΎ (Baseβπ)))} = {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))}) |
17 | 8, 16 | xpeq12d 5665 |
. . . . 5
β’ (π = πΎ β ((((DIsoAβπ)βπ€)βπ₯) Γ {(π β ((LTrnβπ)βπ€) β¦ ( I βΎ (Baseβπ)))}) = ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})) |
18 | 7, 17 | mpteq12dv 5197 |
. . . 4
β’ (π = πΎ β (π₯ β dom ((DIsoAβπ)βπ€) β¦ ((((DIsoAβπ)βπ€)βπ₯) Γ {(π β ((LTrnβπ)βπ€) β¦ ( I βΎ (Baseβπ)))})) = (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))}))) |
19 | 4, 18 | mpteq12dv 5197 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ (π₯ β dom ((DIsoAβπ)βπ€) β¦ ((((DIsoAβπ)βπ€)βπ₯) Γ {(π β ((LTrnβπ)βπ€) β¦ ( I βΎ (Baseβπ)))}))) = (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))) |
20 | | df-dib 39605 |
. . 3
β’ DIsoB =
(π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β dom ((DIsoAβπ)βπ€) β¦ ((((DIsoAβπ)βπ€)βπ₯) Γ {(π β ((LTrnβπ)βπ€) β¦ ( I βΎ (Baseβπ)))})))) |
21 | 19, 20, 3 | mptfvmpt 7179 |
. 2
β’ (πΎ β V β
(DIsoBβπΎ) = (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))) |
22 | 1, 21 | syl 17 |
1
β’ (πΎ β π β (DIsoBβπΎ) = (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))) |