Step | Hyp | Ref
| Expression |
1 | | docaval.n |
. . 3
β’ π = ((ocAβπΎ)βπ) |
2 | | docaval.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
3 | | docaval.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
4 | | docaval.o |
. . . . 5
β’ β₯ =
(ocβπΎ) |
5 | | docaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | 2, 3, 4, 5 | docaffvalN 39992 |
. . . 4
β’ (πΎ β π β (ocAβπΎ) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))) |
7 | 6 | fveq1d 6894 |
. . 3
β’ (πΎ β π β ((ocAβπΎ)βπ) = ((π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))βπ)) |
8 | 1, 7 | eqtrid 2785 |
. 2
β’ (πΎ β π β π = ((π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))βπ)) |
9 | | fveq2 6892 |
. . . . . 6
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
10 | | docaval.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
11 | 9, 10 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β ((LTrnβπΎ)βπ€) = π) |
12 | 11 | pweqd 4620 |
. . . 4
β’ (π€ = π β π« ((LTrnβπΎ)βπ€) = π« π) |
13 | | fveq2 6892 |
. . . . . 6
β’ (π€ = π β ((DIsoAβπΎ)βπ€) = ((DIsoAβπΎ)βπ)) |
14 | | docaval.i |
. . . . . 6
β’ πΌ = ((DIsoAβπΎ)βπ) |
15 | 13, 14 | eqtr4di 2791 |
. . . . 5
β’ (π€ = π β ((DIsoAβπΎ)βπ€) = πΌ) |
16 | 15 | cnveqd 5876 |
. . . . . . . . 9
β’ (π€ = π β β‘((DIsoAβπΎ)βπ€) = β‘πΌ) |
17 | 15 | rneqd 5938 |
. . . . . . . . . . 11
β’ (π€ = π β ran ((DIsoAβπΎ)βπ€) = ran πΌ) |
18 | 17 | rabeqdv 3448 |
. . . . . . . . . 10
β’ (π€ = π β {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§} = {π§ β ran πΌ β£ π₯ β π§}) |
19 | 18 | inteqd 4956 |
. . . . . . . . 9
β’ (π€ = π β β© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§} = β© {π§ β ran πΌ β£ π₯ β π§}) |
20 | 16, 19 | fveq12d 6899 |
. . . . . . . 8
β’ (π€ = π β (β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§}) = (β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) |
21 | 20 | fveq2d 6896 |
. . . . . . 7
β’ (π€ = π β ( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) = ( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§}))) |
22 | | fveq2 6892 |
. . . . . . 7
β’ (π€ = π β ( β₯ βπ€) = ( β₯ βπ)) |
23 | 21, 22 | oveq12d 7427 |
. . . . . 6
β’ (π€ = π β (( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) = (( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ))) |
24 | | id 22 |
. . . . . 6
β’ (π€ = π β π€ = π) |
25 | 23, 24 | oveq12d 7427 |
. . . . 5
β’ (π€ = π β ((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€) = ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)) |
26 | 15, 25 | fveq12d 6899 |
. . . 4
β’ (π€ = π β (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€)) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π))) |
27 | 12, 26 | mpteq12dv 5240 |
. . 3
β’ (π€ = π β (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))) = (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))) |
28 | | eqid 2733 |
. . 3
β’ (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€)))) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€)))) |
29 | 10 | fvexi 6906 |
. . . . 5
β’ π β V |
30 | 29 | pwex 5379 |
. . . 4
β’ π«
π β V |
31 | 30 | mptex 7225 |
. . 3
β’ (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π))) β V |
32 | 27, 28, 31 | fvmpt 6999 |
. 2
β’ (π β π» β ((π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))βπ) = (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))) |
33 | 8, 32 | sylan9eq 2793 |
1
β’ ((πΎ β π β§ π β π») β π = (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))) |