Theorem cdlemk5a

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 3-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemk.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemk.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemk.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemk.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemk.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemk.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	cdlemk.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	cdlemk5a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ≤ ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemk.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemk.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemk.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemk.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemk.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemk.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		cdlemk.m	⊢ ∧ = ( meet ‘ 𝐾 )
9		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
10		simp1r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → 𝑊 ∈ 𝐻 )
11		simp21	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → 𝐹 ∈ 𝑇 )
12		simp22	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → 𝐺 ∈ 𝑇 )
13		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) )
14	1 2 3 4 5 6 7 8	cdlemk3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 𝐹 ‘ 𝑃 ) )
15	9 10 11 12 13 14	syl221anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( 𝐹 ‘ 𝑃 ) )
16		simp23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → 𝑋 ∈ 𝑇 )
17		simp33l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → 𝑃 ∈ 𝐴 )
18		simp33r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ¬ 𝑃 ≤ 𝑊 )
19	1 2 3 4 5 6 7 8	cdlemk4	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) )
20	9 10 11 16 17 18 19	syl222anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ 𝑃 ) ≤ ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) )
21	15 20	eqbrtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ ( ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ) → ( ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ≤ ( ( 𝑋 ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) )