Step | Hyp | Ref
| Expression |
1 | | elex 3492 |
. 2
β’ (πΎ β πΆ β πΎ β V) |
2 | | fveq2 6888 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | ltrnset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2790 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6888 |
. . . . . 6
β’ (π = πΎ β (LDilβπ) = (LDilβπΎ)) |
6 | 5 | fveq1d 6890 |
. . . . 5
β’ (π = πΎ β ((LDilβπ)βπ€) = ((LDilβπΎ)βπ€)) |
7 | | fveq2 6888 |
. . . . . . 7
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
8 | | ltrnset.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
9 | 7, 8 | eqtr4di 2790 |
. . . . . 6
β’ (π = πΎ β (Atomsβπ) = π΄) |
10 | | fveq2 6888 |
. . . . . . . . . . . 12
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
11 | | ltrnset.l |
. . . . . . . . . . . 12
β’ β€ =
(leβπΎ) |
12 | 10, 11 | eqtr4di 2790 |
. . . . . . . . . . 11
β’ (π = πΎ β (leβπ) = β€ ) |
13 | 12 | breqd 5158 |
. . . . . . . . . 10
β’ (π = πΎ β (π(leβπ)π€ β π β€ π€)) |
14 | 13 | notbid 317 |
. . . . . . . . 9
β’ (π = πΎ β (Β¬ π(leβπ)π€ β Β¬ π β€ π€)) |
15 | 12 | breqd 5158 |
. . . . . . . . . 10
β’ (π = πΎ β (π(leβπ)π€ β π β€ π€)) |
16 | 15 | notbid 317 |
. . . . . . . . 9
β’ (π = πΎ β (Β¬ π(leβπ)π€ β Β¬ π β€ π€)) |
17 | 14, 16 | anbi12d 631 |
. . . . . . . 8
β’ (π = πΎ β ((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β (Β¬ π β€ π€ β§ Β¬ π β€ π€))) |
18 | | fveq2 6888 |
. . . . . . . . . . 11
β’ (π = πΎ β (meetβπ) = (meetβπΎ)) |
19 | | ltrnset.m |
. . . . . . . . . . 11
β’ β§ =
(meetβπΎ) |
20 | 18, 19 | eqtr4di 2790 |
. . . . . . . . . 10
β’ (π = πΎ β (meetβπ) = β§ ) |
21 | | fveq2 6888 |
. . . . . . . . . . . 12
β’ (π = πΎ β (joinβπ) = (joinβπΎ)) |
22 | | ltrnset.j |
. . . . . . . . . . . 12
β’ β¨ =
(joinβπΎ) |
23 | 21, 22 | eqtr4di 2790 |
. . . . . . . . . . 11
β’ (π = πΎ β (joinβπ) = β¨ ) |
24 | 23 | oveqd 7422 |
. . . . . . . . . 10
β’ (π = πΎ β (π(joinβπ)(πβπ)) = (π β¨ (πβπ))) |
25 | | eqidd 2733 |
. . . . . . . . . 10
β’ (π = πΎ β π€ = π€) |
26 | 20, 24, 25 | oveq123d 7426 |
. . . . . . . . 9
β’ (π = πΎ β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π β¨ (πβπ)) β§ π€)) |
27 | 23 | oveqd 7422 |
. . . . . . . . . 10
β’ (π = πΎ β (π(joinβπ)(πβπ)) = (π β¨ (πβπ))) |
28 | 20, 27, 25 | oveq123d 7426 |
. . . . . . . . 9
β’ (π = πΎ β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π β¨ (πβπ)) β§ π€)) |
29 | 26, 28 | eqeq12d 2748 |
. . . . . . . 8
β’ (π = πΎ β (((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))) |
30 | 17, 29 | imbi12d 344 |
. . . . . . 7
β’ (π = πΎ β (((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€)) β ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€)))) |
31 | 9, 30 | raleqbidv 3342 |
. . . . . 6
β’ (π = πΎ β (βπ β (Atomsβπ)((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€)) β βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€)))) |
32 | 9, 31 | raleqbidv 3342 |
. . . . 5
β’ (π = πΎ β (βπ β (Atomsβπ)βπ β (Atomsβπ)((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€)) β βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€)))) |
33 | 6, 32 | rabeqbidv 3449 |
. . . 4
β’ (π = πΎ β {π β ((LDilβπ)βπ€) β£ βπ β (Atomsβπ)βπ β (Atomsβπ)((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€))} = {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))}) |
34 | 4, 33 | mpteq12dv 5238 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ {π β ((LDilβπ)βπ€) β£ βπ β (Atomsβπ)βπ β (Atomsβπ)((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€))}) = (π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})) |
35 | | df-ltrn 38964 |
. . 3
β’ LTrn =
(π β V β¦ (π€ β (LHypβπ) β¦ {π β ((LDilβπ)βπ€) β£ βπ β (Atomsβπ)βπ β (Atomsβπ)((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€))})) |
36 | 34, 35, 3 | mptfvmpt 7226 |
. 2
β’ (πΎ β V β
(LTrnβπΎ) = (π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})) |
37 | 1, 36 | syl 17 |
1
β’ (πΎ β πΆ β (LTrnβπΎ) = (π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})) |