Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π· β (πβπ) = (πβπ·)) |
2 | | cdlemk3.o2 |
. . . . . . . . 9
β’ π = (πβπ·) |
3 | 1, 2 | eqtr4di 2791 |
. . . . . . . 8
β’ (π = π· β (πβπ) = π) |
4 | 3 | fveq1d 6845 |
. . . . . . 7
β’ (π = π· β ((πβπ)βπ) = (πβπ)) |
5 | | cnveq 5830 |
. . . . . . . . 9
β’ (π = π· β β‘π = β‘π·) |
6 | 5 | coeq2d 5819 |
. . . . . . . 8
β’ (π = π· β (π β β‘π) = (π β β‘π·)) |
7 | 6 | fveq2d 6847 |
. . . . . . 7
β’ (π = π· β (π
β(π β β‘π)) = (π
β(π β β‘π·))) |
8 | 4, 7 | oveq12d 7376 |
. . . . . 6
β’ (π = π· β (((πβπ)βπ) β¨ (π
β(π β β‘π))) = ((πβπ) β¨ (π
β(π β β‘π·)))) |
9 | 8 | oveq2d 7374 |
. . . . 5
β’ (π = π· β ((π β¨ (π
βπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘π)))) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·))))) |
10 | 9 | eqeq2d 2744 |
. . . 4
β’ (π = π· β ((πβπ) = ((π β¨ (π
βπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘π)))) β (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))))) |
11 | 10 | riotabidv 7316 |
. . 3
β’ (π = π· β (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘π))))) = (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))))) |
12 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΊ β (π
βπ) = (π
βπΊ)) |
13 | 12 | oveq2d 7374 |
. . . . . 6
β’ (π = πΊ β (π β¨ (π
βπ)) = (π β¨ (π
βπΊ))) |
14 | | coeq1 5814 |
. . . . . . . 8
β’ (π = πΊ β (π β β‘π·) = (πΊ β β‘π·)) |
15 | 14 | fveq2d 6847 |
. . . . . . 7
β’ (π = πΊ β (π
β(π β β‘π·)) = (π
β(πΊ β β‘π·))) |
16 | 15 | oveq2d 7374 |
. . . . . 6
β’ (π = πΊ β ((πβπ) β¨ (π
β(π β β‘π·))) = ((πβπ) β¨ (π
β(πΊ β β‘π·)))) |
17 | 13, 16 | oveq12d 7376 |
. . . . 5
β’ (π = πΊ β ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) |
18 | 17 | eqeq2d 2744 |
. . . 4
β’ (π = πΊ β ((πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))) β (πβπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))))) |
19 | 18 | riotabidv 7316 |
. . 3
β’ (π = πΊ β (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·))))) = (β©π β π (πβπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))))) |
20 | | cdlemk3.u1 |
. . 3
β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ (((πβπ)βπ) β¨ (π
β(π β β‘π)))))) |
21 | | riotaex 7318 |
. . 3
β’
(β©π
β π (πβπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·))))) β V |
22 | 11, 19, 20, 21 | ovmpo 7516 |
. 2
β’ ((π· β π β§ πΊ β π) β (π·ππΊ) = (β©π β π (πβπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))))) |
23 | | cdlemk3.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
24 | | cdlemk3.l |
. . . 4
β’ β€ =
(leβπΎ) |
25 | | cdlemk3.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
26 | | cdlemk3.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
27 | | cdlemk3.h |
. . . 4
β’ π» = (LHypβπΎ) |
28 | | cdlemk3.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
29 | | cdlemk3.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
30 | | cdlemk3.m |
. . . 4
β’ β§ =
(meetβπΎ) |
31 | | cdlemk3.u2 |
. . . 4
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘π·)))))) |
32 | 23, 24, 25, 26, 27, 28, 29, 30, 31 | cdlemksv 39353 |
. . 3
β’ (πΊ β π β (πβπΊ) = (β©π β π (πβπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))))) |
33 | 32 | adantl 483 |
. 2
β’ ((π· β π β§ πΊ β π) β (πβπΊ) = (β©π β π (πβπ) = ((π β¨ (π
βπΊ)) β§ ((πβπ) β¨ (π
β(πΊ β β‘π·)))))) |
34 | 22, 33 | eqtr4d 2776 |
1
β’ ((π· β π β§ πΊ β π) β (π·ππΊ) = (πβπΊ)) |