This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ≤ ˙ = ≤ K
trlco.j ⊢ ∨ ˙ = join ⁡ K
trlco.h ⊢ H = LHyp ⁡ K
trlco.t ⊢ T = LTrn ⁡ K ⁡ W
trlco.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlco ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → R ⁡ F ∘ G ≤ ˙ R ⁡ F ∨ ˙ R ⁡ G

Proof

Step Hyp Ref Expression
1 trlco.l ⊢ ≤ ˙ = ≤ K
2 trlco.j ⊢ ∨ ˙ = join ⁡ K
3 trlco.h ⊢ H = LHyp ⁡ K
4 trlco.t ⊢ T = LTrn ⁡ K ⁡ W
5 trlco.r ⊢ R = trL ⁡ K ⁡ W
6 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
7 1 6 3 lhpexnle ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ Atoms ⁡ K ¬ p ≤ ˙ W
8 7 3ad2ant1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → ∃ p ∈ Atoms ⁡ K ¬ p ≤ ˙ W
9 simpl1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W → K ∈ HL ∧ W ∈ H
10 simpl2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W → F ∈ T
11 simpl3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W → G ∈ T
12 simpr ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W → p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W
13 eqid ⊢ meet ⁡ K = meet ⁡ K
14 1 2 3 4 5 13 6 trlcolem ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W → R ⁡ F ∘ G ≤ ˙ R ⁡ F ∨ ˙ R ⁡ G
15 9 10 11 12 14 syl121anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ p ∈ Atoms ⁡ K ∧ ¬ p ≤ ˙ W → R ⁡ F ∘ G ≤ ˙ R ⁡ F ∨ ˙ R ⁡ G
16 8 15 rexlimddv ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T → R ⁡ F ∘ G ≤ ˙ R ⁡ F ∨ ˙ R ⁡ G