Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6843 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | docaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
6 | 5 | fveq1d 6845 |
. . . . . 6
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
7 | 6 | pweqd 4578 |
. . . . 5
β’ (π = πΎ β π« ((LTrnβπ)βπ€) = π« ((LTrnβπΎ)βπ€)) |
8 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (DIsoAβπ) = (DIsoAβπΎ)) |
9 | 8 | fveq1d 6845 |
. . . . . 6
β’ (π = πΎ β ((DIsoAβπ)βπ€) = ((DIsoAβπΎ)βπ€)) |
10 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (meetβπ) = (meetβπΎ)) |
11 | | docaval.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (meetβπ) = β§ ) |
13 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
14 | | docaval.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
15 | 13, 14 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΎ β (joinβπ) = β¨ ) |
16 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = πΎ β (ocβπ) = (ocβπΎ)) |
17 | | docaval.o |
. . . . . . . . . 10
β’ β₯ =
(ocβπΎ) |
18 | 16, 17 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π = πΎ β (ocβπ) = β₯ ) |
19 | 9 | cnveqd 5832 |
. . . . . . . . . 10
β’ (π = πΎ β β‘((DIsoAβπ)βπ€) = β‘((DIsoAβπΎ)βπ€)) |
20 | 9 | rneqd 5894 |
. . . . . . . . . . . 12
β’ (π = πΎ β ran ((DIsoAβπ)βπ€) = ran ((DIsoAβπΎ)βπ€)) |
21 | 20 | rabeqdv 3423 |
. . . . . . . . . . 11
β’ (π = πΎ β {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§} = {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§}) |
22 | 21 | inteqd 4913 |
. . . . . . . . . 10
β’ (π = πΎ β β© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§} = β© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§}) |
23 | 19, 22 | fveq12d 6850 |
. . . . . . . . 9
β’ (π = πΎ β (β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}) = (β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) |
24 | 18, 23 | fveq12d 6850 |
. . . . . . . 8
β’ (π = πΎ β ((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§})) = ( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§}))) |
25 | 18 | fveq1d 6845 |
. . . . . . . 8
β’ (π = πΎ β ((ocβπ)βπ€) = ( β₯ βπ€)) |
26 | 15, 24, 25 | oveq123d 7379 |
. . . . . . 7
β’ (π = πΎ β (((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€)) = (( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€))) |
27 | | eqidd 2738 |
. . . . . . 7
β’ (π = πΎ β π€ = π€) |
28 | 12, 26, 27 | oveq123d 7379 |
. . . . . 6
β’ (π = πΎ β ((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€) = ((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€)) |
29 | 9, 28 | fveq12d 6850 |
. . . . 5
β’ (π = πΎ β (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€)) = (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))) |
30 | 7, 29 | mpteq12dv 5197 |
. . . 4
β’ (π = πΎ β (π₯ β π« ((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€))) = (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€)))) |
31 | 4, 30 | mpteq12dv 5197 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ (π₯ β π« ((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€)))) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))) |
32 | | df-docaN 39586 |
. . 3
β’ ocA =
(π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π« ((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€))))) |
33 | 31, 32, 3 | mptfvmpt 7179 |
. 2
β’ (πΎ β V β
(ocAβπΎ) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))) |
34 | 1, 33 | syl 17 |
1
β’ (πΎ β π β (ocAβπΎ) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))) |