Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme19.l |
⢠⤠= ( le ā š¾ ) |
2 |
|
cdleme19.j |
⢠⨠= ( join ā š¾ ) |
3 |
|
cdleme19.m |
⢠⧠= ( meet ā š¾ ) |
4 |
|
cdleme19.a |
⢠š“ = ( Atoms ā š¾ ) |
5 |
|
cdleme19.h |
⢠š» = ( LHyp ā š¾ ) |
6 |
|
cdleme19.u |
⢠š = ( ( š ⨠š ) ā§ š ) |
7 |
|
cdleme19.f |
⢠š¹ = ( ( š ⨠š ) ā§ ( š ⨠( ( š ⨠š ) ā§ š ) ) ) |
8 |
|
cdleme19.g |
⢠šŗ = ( ( š ⨠š ) ā§ ( š ⨠( ( š ⨠š ) ā§ š ) ) ) |
9 |
|
cdleme19.d |
⢠š· = ( ( š
⨠š ) ā§ š ) |
10 |
|
cdleme19.y |
⢠š = ( ( š
⨠š ) ā§ š ) |
11 |
|
cdleme20.v |
⢠š = ( ( š ⨠š ) ā§ š ) |
12 |
|
simp11l |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š¾ ā HL ) |
13 |
|
simp11r |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š ā š» ) |
14 |
|
simp21l |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š ā š“ ) |
15 |
|
simp21r |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ¬ š ⤠š ) |
16 |
|
simp23l |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š
ā š“ ) |
17 |
|
simp33 |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š
⤠( š ⨠š ) ) |
18 |
|
simp32l |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ¬ š ⤠( š ⨠š ) ) |
19 |
1 2 3 4 5 9
|
cdlemeda |
⢠( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ā§ š
⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ) ā š· ā š“ ) |
20 |
12 13 14 15 16 17 18 19
|
syl223anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š· ā š“ ) |
21 |
2 4
|
hlatjcom |
⢠( ( š¾ ā HL ā§ š· ā š“ ā§ š ā š“ ) ā ( š· ⨠š ) = ( š ⨠š· ) ) |
22 |
12 20 14 21
|
syl3anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š· ⨠š ) = ( š ⨠š· ) ) |
23 |
1 2 3 4 5 9
|
cdleme10 |
⢠( ( ( š¾ ā HL ā§ š ā š» ) ā§ š
ā š“ ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā ( š ⨠š· ) = ( š ⨠š
) ) |
24 |
12 13 16 14 15 23
|
syl212anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ⨠š· ) = ( š ⨠š
) ) |
25 |
22 24
|
eqtrd |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š· ⨠š ) = ( š ⨠š
) ) |
26 |
|
simp22l |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š ā š“ ) |
27 |
|
simp22r |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ¬ š ⤠š ) |
28 |
|
simp32r |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ¬ š ⤠( š ⨠š ) ) |
29 |
1 2 3 4 5 10
|
cdlemeda |
⢠( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ā§ š
⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ) ā š ā š“ ) |
30 |
12 13 26 27 16 17 28 29
|
syl223anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š ā š“ ) |
31 |
2 4
|
hlatjcom |
⢠( ( š¾ ā HL ā§ š ā š“ ā§ š ā š“ ) ā ( š ⨠š ) = ( š ⨠š ) ) |
32 |
12 30 26 31
|
syl3anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ⨠š ) = ( š ⨠š ) ) |
33 |
1 2 3 4 5 10
|
cdleme10 |
⢠( ( ( š¾ ā HL ā§ š ā š» ) ā§ š
ā š“ ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā ( š ⨠š ) = ( š ⨠š
) ) |
34 |
12 13 16 26 27 33
|
syl212anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ⨠š ) = ( š ⨠š
) ) |
35 |
32 34
|
eqtrd |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ⨠š ) = ( š ⨠š
) ) |
36 |
25 35
|
oveq12d |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( ( š· ⨠š ) ā§ ( š ⨠š ) ) = ( ( š ⨠š
) ā§ ( š ⨠š
) ) ) |
37 |
|
simp12l |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š ā š“ ) |
38 |
|
simp13l |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā š ā š“ ) |
39 |
|
simp21 |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ā š“ ⧠¬ š ⤠š ) ) |
40 |
1 2 3 4 5 6 7
|
cdleme1 |
⢠( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ā§ š ā š“ ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ) ā ( š ⨠š¹ ) = ( š ⨠š ) ) |
41 |
12 13 37 38 39 40
|
syl23anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ⨠š¹ ) = ( š ⨠š ) ) |
42 |
|
simp22 |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ā š“ ⧠¬ š ⤠š ) ) |
43 |
1 2 3 4 5 6 8
|
cdleme1 |
⢠( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ā§ š ā š“ ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ) ā ( š ⨠šŗ ) = ( š ⨠š ) ) |
44 |
12 13 37 38 42 43
|
syl23anc |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( š ⨠šŗ ) = ( š ⨠š ) ) |
45 |
41 44
|
oveq12d |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( ( š ⨠š¹ ) ā§ ( š ⨠šŗ ) ) = ( ( š ⨠š ) ā§ ( š ⨠š ) ) ) |
46 |
36 45
|
oveq12d |
⢠( ( ( ( š¾ ā HL ā§ š ā š» ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ) ā§ ( ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š ā š“ ⧠¬ š ⤠š ) ā§ ( š
ā š“ ⧠¬ š
⤠š ) ) ā§ ( ( š ā š ā§ š ā š ) ā§ ( ¬ š ⤠( š ⨠š ) ⧠¬ š ⤠( š ⨠š ) ) ā§ š
⤠( š ⨠š ) ) ) ā ( ( ( š· ⨠š ) ā§ ( š ⨠š ) ) ⨠( ( š ⨠š¹ ) ā§ ( š ⨠šŗ ) ) ) = ( ( ( š ⨠š
) ā§ ( š ⨠š
) ) ⨠( ( š ⨠š ) ā§ ( š ⨠š ) ) ) ) |