Metamath Proof Explorer

Theorem trlcoabs

Description: Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013)

Ref Expression
Hypotheses trlcoabs.l ⊢ ≤ ˙ = ≤ K
trlcoabs.j ⊢ ∨ ˙ = join ⁡ K
trlcoabs.a ⊢ A = Atoms ⁡ K
trlcoabs.h ⊢ H = LHyp ⁡ K
trlcoabs.t ⊢ T = LTrn ⁡ K ⁡ W
trlcoabs.r ⊢ R = trL ⁡ K ⁡ W
Assertion trlcoabs ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∘ G ⁡ P ∨ ˙ R ⁡ F = G ⁡ P ∨ ˙ R ⁡ F

Proof

Step Hyp Ref Expression
1 trlcoabs.l ⊢ ≤ ˙ = ≤ K
2 trlcoabs.j ⊢ ∨ ˙ = join ⁡ K
3 trlcoabs.a ⊢ A = Atoms ⁡ K
4 trlcoabs.h ⊢ H = LHyp ⁡ K
5 trlcoabs.t ⊢ T = LTrn ⁡ K ⁡ W
6 trlcoabs.r ⊢ R = trL ⁡ K ⁡ W
7 1 3 4 5 ltrncoval ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → F ∘ G ⁡ P = F ⁡ G ⁡ P
8 7 3adant3r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∘ G ⁡ P = F ⁡ G ⁡ P
9 8 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∘ G ⁡ P ∨ ˙ R ⁡ F = F ⁡ G ⁡ P ∨ ˙ R ⁡ F
10 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → K ∈ HL ∧ W ∈ H
11 simp2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∈ T
12 1 3 4 5 ltrnel ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W
13 12 3adant2l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W
14 1 2 3 4 5 6 trljat3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ⁡ P ∈ A ∧ ¬ G ⁡ P ≤ ˙ W → G ⁡ P ∨ ˙ R ⁡ F = F ⁡ G ⁡ P ∨ ˙ R ⁡ F
15 10 11 13 14 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → G ⁡ P ∨ ˙ R ⁡ F = F ⁡ G ⁡ P ∨ ˙ R ⁡ F
16 9 15 eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A ∧ ¬ P ≤ ˙ W → F ∘ G ⁡ P ∨ ˙ R ⁡ F = G ⁡ P ∨ ˙ R ⁡ F