cdlemc3

Description: Part of proof of Lemma C in Crawley p. 113. (Contributed by NM, 26-May-2012)

	Ref	Expression
Hypotheses	cdlemc3.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemc3.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemc3.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemc3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemc3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemc3.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemc3.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	cdlemc3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) → 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemc3.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemc3.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemc3.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdlemc3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemc3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemc3.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemc3.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐾 ∈ HL )
9		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		simpr1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝐹 ∈ 𝑇 )
11		simpr2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑃 ∈ 𝐴 )
12	1 4 5 6	ltrnat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
13	9 10 11 12	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
14		simpr3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → 𝑄 ∈ 𝐴 )
15		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16	15 5 6 7	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
17	10 16	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
18	1 4 5 6	ltrnel	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
19	18	3adant3r3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
20	1 4 5 6 7	trlnle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) ) → ¬ ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑅 ‘ 𝐹 ) )
21	9 10 19 20	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ¬ ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑅 ‘ 𝐹 ) )
22	15 1 2 4	hlexch2	⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) → 𝑄 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ) )
23	8 13 14 17 21 22	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) → 𝑄 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ) )
24	1 2 4 5 6 7	trljat2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
25	24	3adant3r3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) )
26	25	breq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( 𝑄 ≤ ( ( 𝐹 ‘ 𝑃 ) ∨ ( 𝑅 ‘ 𝐹 ) ) ↔ 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) )
27	23 26	sylibd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ) → ( ( 𝐹 ‘ 𝑃 ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ 𝐹 ) ) → 𝑄 ≤ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ) )

Metamath Proof Explorer

Theorem cdlemc3

Proof