Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . . . 6
β’ ((π β§ ( β₯ βπ)) = 0 β (π(joinβπΎ)(π β§ ( β₯ βπ))) = (π(joinβπΎ) 0 )) |
2 | 1 | adantl 483 |
. . . . 5
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β§ ( β₯ βπ)) = 0 ) β (π(joinβπΎ)(π β§ ( β₯ βπ))) = (π(joinβπΎ) 0 )) |
3 | | omlol 37705 |
. . . . . . . 8
β’ (πΎ β OML β πΎ β OL) |
4 | | omllaw3.b |
. . . . . . . . 9
β’ π΅ = (BaseβπΎ) |
5 | | eqid 2737 |
. . . . . . . . 9
β’
(joinβπΎ) =
(joinβπΎ) |
6 | | omllaw3.z |
. . . . . . . . 9
β’ 0 =
(0.βπΎ) |
7 | 4, 5, 6 | olj01 37690 |
. . . . . . . 8
β’ ((πΎ β OL β§ π β π΅) β (π(joinβπΎ) 0 ) = π) |
8 | 3, 7 | sylan 581 |
. . . . . . 7
β’ ((πΎ β OML β§ π β π΅) β (π(joinβπΎ) 0 ) = π) |
9 | 8 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π(joinβπΎ) 0 ) = π) |
10 | 9 | adantr 482 |
. . . . 5
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β§ ( β₯ βπ)) = 0 ) β (π(joinβπΎ) 0 ) = π) |
11 | 2, 10 | eqtr2d 2778 |
. . . 4
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β§ ( β₯ βπ)) = 0 ) β π = (π(joinβπΎ)(π β§ ( β₯ βπ)))) |
12 | 11 | adantrl 715 |
. . 3
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ (π β§ ( β₯ βπ)) = 0 )) β π = (π(joinβπΎ)(π β§ ( β₯ βπ)))) |
13 | | omllaw3.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
14 | | omllaw3.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
15 | | omllaw3.o |
. . . . . 6
β’ β₯ =
(ocβπΎ) |
16 | 4, 13, 5, 14, 15 | omllaw 37708 |
. . . . 5
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (π β€ π β π = (π(joinβπΎ)(π β§ ( β₯ βπ))))) |
17 | 16 | imp 408 |
. . . 4
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ π β€ π) β π = (π(joinβπΎ)(π β§ ( β₯ βπ)))) |
18 | 17 | adantrr 716 |
. . 3
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ (π β§ ( β₯ βπ)) = 0 )) β π = (π(joinβπΎ)(π β§ ( β₯ βπ)))) |
19 | 12, 18 | eqtr4d 2780 |
. 2
β’ (((πΎ β OML β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ (π β§ ( β₯ βπ)) = 0 )) β π = π) |
20 | 19 | ex 414 |
1
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β ((π β€ π β§ (π β§ ( β₯ βπ)) = 0 ) β π = π)) |