Theorem cdleme21at

Description: Part of proof of Lemma E in Crawley p. 115. (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	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion	cdleme21at	⊢ ( ( ( ( 𝐾 ∈ 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	1 2 3 4 5 6	cdleme21c	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) )
8	7	3adant2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) )
9		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) )
10		oveq2	⊢ ( 𝑇 = 𝑧 → ( 𝑆 ∨ 𝑇 ) = ( 𝑆 ∨ 𝑧 ) )
11	10	breq2d	⊢ ( 𝑇 = 𝑧 → ( 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ↔ 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) ) )
12	9 11	syl5ibcom	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( 𝑇 = 𝑧 → 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) ) )
13	12	necon3bd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → ( ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑧 ) → 𝑇 ≠ 𝑧 ) )
14	8 13	mpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑧 ) = ( 𝑆 ∨ 𝑧 ) ) ) → 𝑇 ≠ 𝑧 )