Theorem cdleme16g

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, Eq. (1). F and G represent f(s) and f(t) respectively. We show, in their notation, (s \/ t) /\ w=(f(s) \/ f(t)) /\ w. (Contributed by NM, 11-Oct-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme12.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme12.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme12.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme12.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme12.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7		cdleme12.f	⊢ 𝐹 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
8		cdleme12.g	⊢ 𝐺 = ( ( 𝑇 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑇 ) ∧ 𝑊 ) ) )
9	1 2 3 4 5 6 7 8	cdleme16e	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝐹 ∨ 𝐺 ) ) = ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) )
10	1 2 3 4 5 6 7 8	cdleme16f	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ ( 𝐹 ∨ 𝐺 ) ) = ( ( 𝐹 ∨ 𝐺 ) ∧ 𝑊 ) )
11	9 10	eqtr3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ∧ ( 𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑆 ≠ 𝑇 ) ) ∧ ( ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑈 ≤ ( 𝑆 ∨ 𝑇 ) ) ) → ( ( 𝑆 ∨ 𝑇 ) ∧ 𝑊 ) = ( ( 𝐹 ∨ 𝐺 ) ∧ 𝑊 ) )