Step | Hyp | Ref
| Expression |
1 | | dibval.i |
. . 3
β’ πΌ = ((DIsoBβπΎ)βπ) |
2 | | dibval.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | dibval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | dibffval 39606 |
. . . 4
β’ (πΎ β π β (DIsoBβπΎ) = (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))) |
5 | 4 | fveq1d 6845 |
. . 3
β’ (πΎ β π β ((DIsoBβπΎ)βπ) = ((π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))βπ)) |
6 | 1, 5 | eqtrid 2789 |
. 2
β’ (πΎ β π β πΌ = ((π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))βπ)) |
7 | | fveq2 6843 |
. . . . . 6
β’ (π€ = π β ((DIsoAβπΎ)βπ€) = ((DIsoAβπΎ)βπ)) |
8 | | dibval.j |
. . . . . 6
β’ π½ = ((DIsoAβπΎ)βπ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β ((DIsoAβπΎ)βπ€) = π½) |
10 | 9 | dmeqd 5862 |
. . . 4
β’ (π€ = π β dom ((DIsoAβπΎ)βπ€) = dom π½) |
11 | 9 | fveq1d 6845 |
. . . . 5
β’ (π€ = π β (((DIsoAβπΎ)βπ€)βπ₯) = (π½βπ₯)) |
12 | | fveq2 6843 |
. . . . . . . . 9
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
13 | | dibval.t |
. . . . . . . . 9
β’ π = ((LTrnβπΎ)βπ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . 8
β’ (π€ = π β ((LTrnβπΎ)βπ€) = π) |
15 | | eqidd 2738 |
. . . . . . . 8
β’ (π€ = π β ( I βΎ π΅) = ( I βΎ π΅)) |
16 | 14, 15 | mpteq12dv 5197 |
. . . . . . 7
β’ (π€ = π β (π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅)) = (π β π β¦ ( I βΎ π΅))) |
17 | | dibval.o |
. . . . . . 7
β’ 0 = (π β π β¦ ( I βΎ π΅)) |
18 | 16, 17 | eqtr4di 2795 |
. . . . . 6
β’ (π€ = π β (π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅)) = 0 ) |
19 | 18 | sneqd 4599 |
. . . . 5
β’ (π€ = π β {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))} = { 0 }) |
20 | 11, 19 | xpeq12d 5665 |
. . . 4
β’ (π€ = π β ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))}) = ((π½βπ₯) Γ { 0 })) |
21 | 10, 20 | mpteq12dv 5197 |
. . 3
β’ (π€ = π β (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})) = (π₯ β dom π½ β¦ ((π½βπ₯) Γ { 0 }))) |
22 | | eqid 2737 |
. . 3
β’ (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))}))) = (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))}))) |
23 | 8 | fvexi 6857 |
. . . . 5
β’ π½ β V |
24 | 23 | dmex 7849 |
. . . 4
β’ dom π½ β V |
25 | 24 | mptex 7174 |
. . 3
β’ (π₯ β dom π½ β¦ ((π½βπ₯) Γ { 0 })) β
V |
26 | 21, 22, 25 | fvmpt 6949 |
. 2
β’ (π β π» β ((π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))βπ) = (π₯ β dom π½ β¦ ((π½βπ₯) Γ { 0 }))) |
27 | 6, 26 | sylan9eq 2797 |
1
β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β dom π½ β¦ ((π½βπ₯) Γ { 0 }))) |