Theorem cdleme3fN

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . TODO: Delete - duplicates cdleme0e . (Contributed by NM, 6-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme1.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme1.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme1.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme1.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme1.f	⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
	cdleme3.3	⊢ 𝑉 = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 )
Assertion	cdleme3fN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑈 ≠ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme1.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme1.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme1.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme1.f	⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
8		cdleme3.3	⊢ 𝑉 = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 )
9	1 2 3 4 5 6 8	cdleme0e	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑈 ≠ 𝑉 )