Theorem trlco

Description: The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of Crawley p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013)

	Ref	Expression
Hypotheses	trlco.l	⊢ ≤ = ( le ‘ 𝐾 )
	trlco.j	⊢ ∨ = ( join ‘ 𝐾 )
	trlco.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	trlco.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	trlco.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	trlco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		trlco.l	⊢ ≤ = ( le ‘ 𝐾 )
2		trlco.j	⊢ ∨ = ( join ‘ 𝐾 )
3		trlco.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		trlco.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		trlco.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7	1 6 3	lhpexnle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑝 ≤ 𝑊 )
8	7	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑝 ≤ 𝑊 )
9		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		simpl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
11		simpl3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
12		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) )
13		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
14	1 2 3 4 5 13 6	trlcolem	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
15	9 10 11 12 14	syl121anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
16	8 15	rexlimddv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐹 ∘ 𝐺 ) ) ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )