Step |
Hyp |
Ref |
Expression |
1 |
|
2atmatz.j |
|- .\/ = ( join ` K ) |
2 |
|
2atmatz.m |
|- ./\ = ( meet ` K ) |
3 |
|
2atmatz.z |
|- .0. = ( 0. ` K ) |
4 |
|
2atmatz.a |
|- A = ( Atoms ` K ) |
5 |
|
simpl |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( K e. HL /\ P e. A /\ Q e. A ) ) |
6 |
|
simpr1 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> R e. A ) |
7 |
|
simpr2 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> S e. A ) |
8 |
7
|
orcd |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( S e. A \/ S = .0. ) ) |
9 |
|
simpr3 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( P .\/ Q ) =/= ( R .\/ S ) ) |
10 |
1 2 3 4
|
2at0mat0 |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ ( S e. A \/ S = .0. ) /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) ) |
11 |
5 6 8 9 10
|
syl13anc |
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ ( P .\/ Q ) =/= ( R .\/ S ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A \/ ( ( P .\/ Q ) ./\ ( R .\/ S ) ) = .0. ) ) |