Step | Hyp | Ref
| Expression |
1 | | djaval.j |
. . 3
β’ π½ = ((vAβπΎ)βπ) |
2 | | djaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | 2 | djaffvalN 39534 |
. . . 4
β’ (πΎ β π β (vAβπΎ) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦)))))) |
4 | 3 | fveq1d 6841 |
. . 3
β’ (πΎ β π β ((vAβπΎ)βπ) = ((π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦)))))βπ)) |
5 | 1, 4 | eqtrid 2789 |
. 2
β’ (πΎ β π β π½ = ((π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦)))))βπ)) |
6 | | fveq2 6839 |
. . . . . 6
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
7 | | djaval.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β ((LTrnβπΎ)βπ€) = π) |
9 | 8 | pweqd 4575 |
. . . 4
β’ (π€ = π β π« ((LTrnβπΎ)βπ€) = π« π) |
10 | | fveq2 6839 |
. . . . . 6
β’ (π€ = π β ((ocAβπΎ)βπ€) = ((ocAβπΎ)βπ)) |
11 | | djaval.n |
. . . . . 6
β’ β₯ =
((ocAβπΎ)βπ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . 5
β’ (π€ = π β ((ocAβπΎ)βπ€) = β₯ ) |
13 | 12 | fveq1d 6841 |
. . . . . 6
β’ (π€ = π β (((ocAβπΎ)βπ€)βπ₯) = ( β₯ βπ₯)) |
14 | 12 | fveq1d 6841 |
. . . . . 6
β’ (π€ = π β (((ocAβπΎ)βπ€)βπ¦) = ( β₯ βπ¦)) |
15 | 13, 14 | ineq12d 4171 |
. . . . 5
β’ (π€ = π β ((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦)) = (( β₯ βπ₯) β© ( β₯ βπ¦))) |
16 | 12, 15 | fveq12d 6846 |
. . . 4
β’ (π€ = π β (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦))) = ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦)))) |
17 | 9, 9, 16 | mpoeq123dv 7426 |
. . 3
β’ (π€ = π β (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦)))) = (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))) |
18 | | eqid 2737 |
. . 3
β’ (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦))))) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦))))) |
19 | 7 | fvexi 6853 |
. . . . 5
β’ π β V |
20 | 19 | pwex 5333 |
. . . 4
β’ π«
π β V |
21 | 20, 20 | mpoex 8004 |
. . 3
β’ (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦)))) β
V |
22 | 17, 18, 21 | fvmpt 6945 |
. 2
β’ (π β π» β ((π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦)))))βπ) = (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))) |
23 | 5, 22 | sylan9eq 2797 |
1
β’ ((πΎ β π β§ π β π») β π½ = (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))) |