Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β πΆ β πΎ β V) |
2 | | fveq2 6843 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | trlset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6843 |
. . . . . 6
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
6 | 5 | fveq1d 6845 |
. . . . 5
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
7 | | fveq2 6843 |
. . . . . . 7
β’ (π = πΎ β (Baseβπ) = (BaseβπΎ)) |
8 | | trlset.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
9 | 7, 8 | eqtr4di 2795 |
. . . . . 6
β’ (π = πΎ β (Baseβπ) = π΅) |
10 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
11 | | trlset.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (Atomsβπ) = π΄) |
13 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
14 | | trlset.l |
. . . . . . . . . . 11
β’ β€ =
(leβπΎ) |
15 | 13, 14 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = πΎ β (leβπ) = β€ ) |
16 | 15 | breqd 5117 |
. . . . . . . . 9
β’ (π = πΎ β (π(leβπ)π€ β π β€ π€)) |
17 | 16 | notbid 318 |
. . . . . . . 8
β’ (π = πΎ β (Β¬ π(leβπ)π€ β Β¬ π β€ π€)) |
18 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = πΎ β (meetβπ) = (meetβπΎ)) |
19 | | trlset.m |
. . . . . . . . . . 11
β’ β§ =
(meetβπΎ) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = πΎ β (meetβπ) = β§ ) |
21 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
22 | | trlset.j |
. . . . . . . . . . . 12
β’ β¨ =
(joinβπΎ) |
23 | 21, 22 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (π = πΎ β (joinβπ) = β¨ ) |
24 | 23 | oveqd 7375 |
. . . . . . . . . 10
β’ (π = πΎ β (π(joinβπ)(πβπ)) = (π β¨ (πβπ))) |
25 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π = πΎ β π€ = π€) |
26 | 20, 24, 25 | oveq123d 7379 |
. . . . . . . . 9
β’ (π = πΎ β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π β¨ (πβπ)) β§ π€)) |
27 | 26 | eqeq2d 2748 |
. . . . . . . 8
β’ (π = πΎ β (π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€) β π₯ = ((π β¨ (πβπ)) β§ π€))) |
28 | 17, 27 | imbi12d 345 |
. . . . . . 7
β’ (π = πΎ β ((Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€)) β (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))) |
29 | 12, 28 | raleqbidv 3320 |
. . . . . 6
β’ (π = πΎ β (βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€)) β βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))) |
30 | 9, 29 | riotaeqbidv 7317 |
. . . . 5
β’ (π = πΎ β (β©π₯ β (Baseβπ)βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€))) = (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))) |
31 | 6, 30 | mpteq12dv 5197 |
. . . 4
β’ (π = πΎ β (π β ((LTrnβπ)βπ€) β¦ (β©π₯ β (Baseβπ)βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€)))) = (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€))))) |
32 | 4, 31 | mpteq12dv 5197 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ (π β ((LTrnβπ)βπ€) β¦ (β©π₯ β (Baseβπ)βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€))))) = (π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))) |
33 | | df-trl 38625 |
. . 3
β’ trL =
(π β V β¦ (π€ β (LHypβπ) β¦ (π β ((LTrnβπ)βπ€) β¦ (β©π₯ β (Baseβπ)βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€)))))) |
34 | 32, 33, 3 | mptfvmpt 7179 |
. 2
β’ (πΎ β V β
(trLβπΎ) = (π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))) |
35 | 1, 34 | syl 17 |
1
β’ (πΎ β πΆ β (trLβπΎ) = (π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))) |