| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cdlemk1.b |
β’ π΅ = ( Base β πΎ ) |
| 2 |
|
cdlemk1.l |
β’ β€ = ( le β πΎ ) |
| 3 |
|
cdlemk1.j |
β’ β¨ = ( join β πΎ ) |
| 4 |
|
cdlemk1.m |
β’ β§ = ( meet β πΎ ) |
| 5 |
|
cdlemk1.a |
β’ π΄ = ( Atoms β πΎ ) |
| 6 |
|
cdlemk1.h |
β’ π» = ( LHyp β πΎ ) |
| 7 |
|
cdlemk1.t |
β’ π = ( ( LTrn β πΎ ) β π ) |
| 8 |
|
cdlemk1.r |
β’ π
= ( ( trL β πΎ ) β π ) |
| 9 |
|
cdlemk1.s |
β’ π = ( π β π β¦ ( β© π β π ( π β π ) = ( ( π β¨ ( π
β π ) ) β§ ( ( π β π ) β¨ ( π
β ( π β β‘ πΉ ) ) ) ) ) ) |
| 10 |
|
cdlemk1.o |
β’ π = ( π β π· ) |
| 11 |
|
simp11l |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β πΎ β HL ) |
| 12 |
11
|
hllatd |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β πΎ β Lat ) |
| 13 |
|
simp22l |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β π β π΄ ) |
| 14 |
|
simp1 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) ) |
| 15 |
|
simp211 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β π β π ) |
| 16 |
|
simp22 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π β π΄ β§ Β¬ π β€ π ) ) |
| 17 |
|
simp23 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π
β πΉ ) = ( π
β π ) ) |
| 18 |
15 16 17
|
3jca |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π β π β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) ) |
| 19 |
|
simp3l1 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β πΉ β ( I βΎ π΅ ) ) |
| 20 |
|
simp3l2 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β π· β ( I βΎ π΅ ) ) |
| 21 |
|
simp3r1 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π
β π· ) β ( π
β πΉ ) ) |
| 22 |
19 20 21
|
3jca |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ ( π
β π· ) β ( π
β πΉ ) ) ) |
| 23 |
1 2 3 4 5 6 7 8 9 10
|
cdlemkoatnle |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( π β π β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ ( π
β π· ) β ( π
β πΉ ) ) ) β ( ( π β π ) β π΄ β§ Β¬ ( π β π ) β€ π ) ) |
| 24 |
23
|
simpld |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( π β π β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ ( π
β π· ) β ( π
β πΉ ) ) ) β ( π β π ) β π΄ ) |
| 25 |
14 18 22 24
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π β π ) β π΄ ) |
| 26 |
1 3 5
|
hlatjcl |
β’ ( ( πΎ β HL β§ π β π΄ β§ ( π β π ) β π΄ ) β ( π β¨ ( π β π ) ) β π΅ ) |
| 27 |
11 13 25 26
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π β¨ ( π β π ) ) β π΅ ) |
| 28 |
|
simp11 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( πΎ β HL β§ π β π» ) ) |
| 29 |
|
simp212 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β πΊ β π ) |
| 30 |
2 5 6 7
|
ltrnat |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ πΊ β π β§ π β π΄ ) β ( πΊ β π ) β π΄ ) |
| 31 |
28 29 13 30
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( πΊ β π ) β π΄ ) |
| 32 |
|
simp13 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β π· β π ) |
| 33 |
|
simp3r2 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π
β πΊ ) β ( π
β π· ) ) |
| 34 |
5 6 7 8
|
trlcocnvat |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ ( πΊ β π β§ π· β π ) β§ ( π
β πΊ ) β ( π
β π· ) ) β ( π
β ( πΊ β β‘ π· ) ) β π΄ ) |
| 35 |
28 29 32 33 34
|
syl121anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π
β ( πΊ β β‘ π· ) ) β π΄ ) |
| 36 |
1 3 5
|
hlatjcl |
β’ ( ( πΎ β HL β§ ( πΊ β π ) β π΄ β§ ( π
β ( πΊ β β‘ π· ) ) β π΄ ) β ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) β π΅ ) |
| 37 |
11 31 35 36
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) β π΅ ) |
| 38 |
1 4
|
latmcl |
β’ ( ( πΎ β Lat β§ ( π β¨ ( π β π ) ) β π΅ β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) β π΅ ) β ( ( π β¨ ( π β π ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β π΅ ) |
| 39 |
12 27 37 38
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π β¨ ( π β π ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β π΅ ) |
| 40 |
2 5 6 7
|
ltrnat |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ π· β π β§ π β π΄ ) β ( π· β π ) β π΄ ) |
| 41 |
28 32 13 40
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π· β π ) β π΄ ) |
| 42 |
1 5 6 7 8
|
trlnidat |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ π· β π β§ π· β ( I βΎ π΅ ) ) β ( π
β π· ) β π΄ ) |
| 43 |
28 32 20 42
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π
β π· ) β π΄ ) |
| 44 |
1 3 5
|
hlatjcl |
β’ ( ( πΎ β HL β§ ( π· β π ) β π΄ β§ ( π
β π· ) β π΄ ) β ( ( π· β π ) β¨ ( π
β π· ) ) β π΅ ) |
| 45 |
11 41 43 44
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π· β π ) β¨ ( π
β π· ) ) β π΅ ) |
| 46 |
1 3 5
|
hlatjcl |
β’ ( ( πΎ β HL β§ ( π· β π ) β π΄ β§ ( π
β ( πΊ β β‘ π· ) ) β π΄ ) β ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) β π΅ ) |
| 47 |
11 41 35 46
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) β π΅ ) |
| 48 |
1 4
|
latmcl |
β’ ( ( πΎ β Lat β§ ( ( π· β π ) β¨ ( π
β π· ) ) β π΅ β§ ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) β π΅ ) β ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β π΅ ) |
| 49 |
12 45 47 48
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β π΅ ) |
| 50 |
|
simp213 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β π β π ) |
| 51 |
2 5 6 7
|
ltrnat |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ π β π β§ π β π΄ ) β ( π β π ) β π΄ ) |
| 52 |
28 50 13 51
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π β π ) β π΄ ) |
| 53 |
|
simp3r3 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π
β π ) β ( π
β π· ) ) |
| 54 |
5 6 7 8
|
trlcocnvat |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ ( π β π β§ π· β π ) β§ ( π
β π ) β ( π
β π· ) ) β ( π
β ( π β β‘ π· ) ) β π΄ ) |
| 55 |
28 50 32 53 54
|
syl121anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π
β ( π β β‘ π· ) ) β π΄ ) |
| 56 |
1 3 5
|
hlatjcl |
β’ ( ( πΎ β HL β§ ( π β π ) β π΄ β§ ( π
β ( π β β‘ π· ) ) β π΄ ) β ( ( π β π ) β¨ ( π
β ( π β β‘ π· ) ) ) β π΅ ) |
| 57 |
11 52 55 56
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π β π ) β¨ ( π
β ( π β β‘ π· ) ) ) β π΅ ) |
| 58 |
1 2 3 4 5 6 7 8 9 10
|
cdlemk1u |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( π β π β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ ( π
β π· ) β ( π
β πΉ ) ) ) β ( π β¨ ( π β π ) ) β€ ( ( π· β π ) β¨ ( π
β π· ) ) ) |
| 59 |
14 18 22 58
|
syl3anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π β¨ ( π β π ) ) β€ ( ( π· β π ) β¨ ( π
β π· ) ) ) |
| 60 |
1 2 4
|
latmlem1 |
β’ ( ( πΎ β Lat β§ ( ( π β¨ ( π β π ) ) β π΅ β§ ( ( π· β π ) β¨ ( π
β π· ) ) β π΅ β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) β π΅ ) ) β ( ( π β¨ ( π β π ) ) β€ ( ( π· β π ) β¨ ( π
β π· ) ) β ( ( π β¨ ( π β π ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β€ ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) ) ) |
| 61 |
12 27 45 37 60
|
syl13anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π β¨ ( π β π ) ) β€ ( ( π· β π ) β¨ ( π
β π· ) ) β ( ( π β¨ ( π β π ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β€ ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) ) ) |
| 62 |
59 61
|
mpd |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π β¨ ( π β π ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β€ ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) ) |
| 63 |
|
simp11r |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β π β π» ) |
| 64 |
1 2 3 5 6 7 8
|
cdlemk2 |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ ( π· β π β§ πΊ β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) ) β ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) = ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) |
| 65 |
11 63 32 29 16 64
|
syl221anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) = ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) |
| 66 |
65
|
oveq2d |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) = ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) ) |
| 67 |
62 66
|
breqtrd |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π β¨ ( π β π ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β€ ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) ) |
| 68 |
|
simp3l3 |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β πΊ β ( I βΎ π΅ ) ) |
| 69 |
20 68
|
jca |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) ) |
| 70 |
1 2 3 5 6 7 8 4
|
cdlemk5a |
β’ ( ( ( πΎ β HL β§ π β π» ) β§ ( π· β π β§ πΊ β π β§ π β π ) β§ ( ( π
β πΊ ) β ( π
β π· ) β§ ( π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( π β π΄ β§ Β¬ π β€ π ) ) ) β ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β€ ( ( π β π ) β¨ ( π
β ( π β β‘ π· ) ) ) ) |
| 71 |
11 63 32 29 50 33 69 16 70
|
syl233anc |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( ( π· β π ) β¨ ( π
β π· ) ) β§ ( ( π· β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β€ ( ( π β π ) β¨ ( π
β ( π β β‘ π· ) ) ) ) |
| 72 |
1 2 12 39 49 57 67 71
|
lattrd |
β’ ( ( ( ( πΎ β HL β§ π β π» ) β§ πΉ β π β§ π· β π ) β§ ( ( π β π β§ πΊ β π β§ π β π ) β§ ( π β π΄ β§ Β¬ π β€ π ) β§ ( π
β πΉ ) = ( π
β π ) ) β§ ( ( πΉ β ( I βΎ π΅ ) β§ π· β ( I βΎ π΅ ) β§ πΊ β ( I βΎ π΅ ) ) β§ ( ( π
β π· ) β ( π
β πΉ ) β§ ( π
β πΊ ) β ( π
β π· ) β§ ( π
β π ) β ( π
β π· ) ) ) ) β ( ( π β¨ ( π β π ) ) β§ ( ( πΊ β π ) β¨ ( π
β ( πΊ β β‘ π· ) ) ) ) β€ ( ( π β π ) β¨ ( π
β ( π β β‘ π· ) ) ) ) |