cdleme28b

Description: Lemma for cdleme25b . TODO: FIX COMMENT. (Contributed by NM, 6-Feb-2013)

	Ref	Expression
Hypotheses	cdleme26.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdleme26.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme26.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme26.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme26.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme26.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme27.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme27.f	⊢ 𝐹 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
	cdleme27.z	⊢ 𝑍 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme27.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑠 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme27.d	⊢ 𝐷 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
	cdleme27.c	⊢ 𝐶 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐷 , 𝐹 )
	cdleme27.g	⊢ 𝐺 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
	cdleme27.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑡 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme27.e	⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
	cdleme27.y	⊢ 𝑌 = if ( 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐸 , 𝐺 )
Assertion	cdleme28b	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑌 ∨ ( 𝑋 ∧ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdleme26.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdleme26.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdleme26.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdleme26.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdleme26.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		cdleme27.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8		cdleme27.f	⊢ 𝐹 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
9		cdleme27.z	⊢ 𝑍 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
10		cdleme27.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑠 ∨ 𝑧 ) ∧ 𝑊 ) ) )
11		cdleme27.d	⊢ 𝐷 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
12		cdleme27.c	⊢ 𝐶 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐷 , 𝐹 )
13		cdleme27.g	⊢ 𝐺 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
14		cdleme27.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑡 ∨ 𝑧 ) ∧ 𝑊 ) ) )
15		cdleme27.e	⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
16		cdleme27.y	⊢ 𝑌 = if ( 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐸 , 𝐺 )
17		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
18	17	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝐾 ∈ Lat )
19		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝑊 ∈ 𝐻 )
20		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
21		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
22		simp22	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) )
23		simp21	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝑃 ≠ 𝑄 )
24	1 2 3 4 5 6 7 8 9 10 11 12	cdleme27cl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝐶 ∈ 𝐵 )
25	17 19 20 21 22 23 24	syl222anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝐶 ∈ 𝐵 )
26		simp33l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝑋 ∈ 𝐵 )
27	1 6	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
28	19 27	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝑊 ∈ 𝐵 )
29	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
30	18 26 28 29	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
31	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝐶 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
32	18 25 30 31	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
33		simp23	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) )
34	1 2 3 4 5 6 7 13 9 14 15 16	cdleme27cl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ) ) → 𝑌 ∈ 𝐵 )
35	17 19 20 21 33 23 34	syl222anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝑌 ∈ 𝐵 )
36	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ) → ( 𝑌 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
37	18 35 30 36	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑌 ∨ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝐵 )
38		eqid	⊢ ( ( 𝑠 ∨ 𝑡 ) ∧ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝑠 ∨ 𝑡 ) ∧ ( 𝑋 ∧ 𝑊 ) )
39	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 38	cdleme28a	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝑌 ∨ ( 𝑋 ∧ 𝑊 ) ) )
40		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
41		simp31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝑠 ≠ 𝑡 )
42	41	necomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → 𝑡 ≠ 𝑠 )
43		simp32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
44	43	ancomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) )
45		simp33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) )
46		eqid	⊢ ( ( 𝑡 ∨ 𝑠 ) ∧ ( 𝑋 ∧ 𝑊 ) ) = ( ( 𝑡 ∨ 𝑠 ) ∧ ( 𝑋 ∧ 𝑊 ) )
47	1 2 3 4 5 6 7 13 9 14 15 16 8 10 11 12 46	cdleme28a	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ) ∧ ( 𝑡 ≠ 𝑠 ∧ ( ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑌 ∨ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) )
48	40 20 21 23 33 22 42 44 45 47	syl333anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝑌 ∨ ( 𝑋 ∧ 𝑊 ) ) ≤ ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) )
49	1 2 18 32 37 39 48	latasymd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ¬ 𝑠 ≤ 𝑊 ) ∧ ( 𝑡 ∈ 𝐴 ∧ ¬ 𝑡 ≤ 𝑊 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ ( ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ∧ ( 𝑡 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ) → ( 𝐶 ∨ ( 𝑋 ∧ 𝑊 ) ) = ( 𝑌 ∨ ( 𝑋 ∧ 𝑊 ) ) )

Metamath Proof Explorer

Theorem cdleme28b

Proof