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