Step | Hyp | Ref
| Expression |
1 | | djaval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | djaval.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
3 | | djaval.i |
. . . . 5
β’ πΌ = ((DIsoAβπΎ)βπ) |
4 | | djaval.n |
. . . . 5
β’ β₯ =
((ocAβπΎ)βπ) |
5 | | djaval.j |
. . . . 5
β’ π½ = ((vAβπΎ)βπ) |
6 | 1, 2, 3, 4, 5 | djafvalN 39600 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π½ = (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))) |
7 | 6 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β π½ = (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))) |
8 | 7 | oveqd 7375 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β (ππ½π) = (π(π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))π)) |
9 | 2 | fvexi 6857 |
. . . . . 6
β’ π β V |
10 | 9 | elpw2 5303 |
. . . . 5
β’ (π β π« π β π β π) |
11 | 10 | biimpri 227 |
. . . 4
β’ (π β π β π β π« π) |
12 | 11 | ad2antrl 727 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β π β π« π) |
13 | 9 | elpw2 5303 |
. . . . 5
β’ (π β π« π β π β π) |
14 | 13 | biimpri 227 |
. . . 4
β’ (π β π β π β π« π) |
15 | 14 | ad2antll 728 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β π β π« π) |
16 | | fvexd 6858 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β ( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β
V) |
17 | | fveq2 6843 |
. . . . . 6
β’ (π₯ = π β ( β₯ βπ₯) = ( β₯ βπ)) |
18 | 17 | ineq1d 4172 |
. . . . 5
β’ (π₯ = π β (( β₯ βπ₯) β© ( β₯ βπ¦)) = (( β₯ βπ) β© ( β₯ βπ¦))) |
19 | 18 | fveq2d 6847 |
. . . 4
β’ (π₯ = π β ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))) = ( β₯
β(( β₯ βπ) β© ( β₯ βπ¦)))) |
20 | | fveq2 6843 |
. . . . . 6
β’ (π¦ = π β ( β₯ βπ¦) = ( β₯ βπ)) |
21 | 20 | ineq2d 4173 |
. . . . 5
β’ (π¦ = π β (( β₯ βπ) β© ( β₯ βπ¦)) = (( β₯ βπ) β© ( β₯ βπ))) |
22 | 21 | fveq2d 6847 |
. . . 4
β’ (π¦ = π β ( β₯ β(( β₯
βπ) β© ( β₯
βπ¦))) = ( β₯
β(( β₯ βπ) β© ( β₯ βπ)))) |
23 | | eqid 2737 |
. . . 4
β’ (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦)))) = (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦)))) |
24 | 19, 22, 23 | ovmpog 7515 |
. . 3
β’ ((π β π« π β§ π β π« π β§ ( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β V)
β (π(π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))π) = ( β₯ β(( β₯
βπ) β© ( β₯
βπ)))) |
25 | 12, 15, 16, 24 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β (π(π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯
βπ₯) β© ( β₯
βπ¦))))π) = ( β₯ β(( β₯
βπ) β© ( β₯
βπ)))) |
26 | 8, 25 | eqtrd 2777 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β (ππ½π) = ( β₯ β(( β₯
βπ) β© ( β₯
βπ)))) |