Theorem cdleme35g

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme35.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme35.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme35.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme35.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme35.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme35.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme35.f	⊢ 𝐹 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
8	1 2 3 4 5 6 7	cdleme35a	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐹 ∨ 𝑈 ) = ( 𝑅 ∨ 𝑈 ) )
9	1 2 3 4 5 6 7	cdleme35e	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∨ ( ( 𝑄 ∨ 𝐹 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑅 ) )
10	8 9	oveq12d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝐹 ∨ 𝑈 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝐹 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑃 ∨ 𝑅 ) ) )
11	1 2 3 4 5 6 7	cdleme35f	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑃 ∨ 𝑅 ) ) = 𝑅 )
12	10 11	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝐹 ∨ 𝑈 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝐹 ) ∧ 𝑊 ) ) ) = 𝑅 )