Theorem cdleme19f

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, line 3. D , F , N , Y , G , O represent s_2, f(s), f_s(r), t_2, f(t), f_t(r). We prove that if r <_ s \/ t, then f_t(r) = f_t(r). (Contributed by NM, 14-Nov-2012)

	Ref	Expression
Hypotheses	cdleme19.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme19.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme19.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme19.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme19.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme19.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme19.f	⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
	cdleme19.g	⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
	cdleme19.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
	cdleme19.y	⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
	cdleme19.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
	cdleme19.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ 𝑌 ) )
Assertion	cdleme19f	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) → 𝑁 = 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		cdleme19.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme19.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme19.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme19.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme19.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme19.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme19.f	⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8		cdleme19.g	⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
9		cdleme19.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
10		cdleme19.y	⊢ 𝑌 = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 )
11		cdleme19.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) )
12		cdleme19.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ 𝑌 ) )
13	1 2 3 4 5 6 7 8 9 10	cdleme19e	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) → ( 𝐹 ∨ 𝐷 ) = ( 𝐺 ∨ 𝑌 ) )
14	13	oveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐹 ∨ 𝐷 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐺 ∨ 𝑌 ) ) )
15	14 11 12	3eqtr4g	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ 𝑅 ∈ 𝐴 ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ∧ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑅 ≤ ( 𝑆 ∨ 𝑇 ) ) ) ) → 𝑁 = 𝑂 )