cdleme21d

Description: Part of proof of Lemma E in Crawley p. 113, last paragraph on p. 115, 3rd line. D , F , N , E , B , Z represent s_2, f(s), f_s(r), z_2, f(z), f_z(r) respectively. We prove f_s(r) = f_z(r). (Contributed by NM, 29-Nov-2012)

	Ref	Expression
Hypotheses	cdleme21.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme21.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme21.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme21.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme21.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme21.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme21.f	⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
	cdleme21.b	⊢ 𝐵 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme21.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
	cdleme21.e	⊢ 𝐸 = ( ( 𝑅 ∨ 𝑧 ) ∧ 𝑊 )
	cdleme21d.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
	cdleme21d.z	⊢ 𝑍 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐵 ∨ 𝐸 ) )
Assertion	cdleme21d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑁 = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme21.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme21.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme21.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme21.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme21.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme21.f	⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8		cdleme21.b	⊢ 𝐵 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
9		cdleme21.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
10		cdleme21.e	⊢ 𝐸 = ( ( 𝑅 ∨ 𝑧 ) ∧ 𝑊 )
11		cdleme21d.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
12		cdleme21d.z	⊢ 𝑍 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐵 ∨ 𝐸 ) )
13		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
15		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
16		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
17		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) )
18		simp33l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) )
19		simp31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑃 ≠ 𝑄 )
20		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝐾 ∈ HL )
21		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑃 ∈ 𝐴 )
22		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑄 ∈ 𝐴 )
23		simp2rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑆 ∈ 𝐴 )
24		simp32l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) )
25	18	simpld	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑧 ∈ 𝐴 )
26		simp33r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) )
27	1 2 4	cdleme21a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → 𝑆 ≠ 𝑧 )
28	20 21 22 23 24 25 26 27	syl322anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑆 ≠ 𝑧 )
29	19 28	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑧 ) )
30	1 2 4	cdleme21b	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) )
31	20 21 22 23 19 24 25 26 30	syl332anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) )
32		simp32r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
33	24 31 32	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
34	1 2 3 4 5 6	cdleme21c	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) )
35	13 14 22 23 19 24 25 26 34	syl332anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) )
36		eqid	⊢ ( ( 𝑆 ∨ 𝑧 ) ∧ 𝑊 ) = ( ( 𝑆 ∨ 𝑧 ) ∧ 𝑊 )
37	1 2 3 4 5 6 7 8 9 10 36 11 12	cdleme20	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑧 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) ) ) → 𝑁 = 𝑍 )
38	13 14 15 16 17 18 29 33 35 37	syl333anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ≤ 𝑊 ) ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) ) → 𝑁 = 𝑍 )

Metamath Proof Explorer

Theorem cdleme21d

Proof