Metamath Proof Explorer

Theorem ltrncoval

Description: Two ways to express value of translation composition. (Contributed by NM, 31-May-2013)

Ref Expression
Hypotheses ltrnel.l ⊢ ≤ ˙ = ≤ K
ltrnel.a ⊢ A = Atoms ⁡ K
ltrnel.h ⊢ H = LHyp ⁡ K
ltrnel.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrncoval ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → F ∘ G ⁡ P = F ⁡ G ⁡ P

Proof

Step Hyp Ref Expression
1 ltrnel.l ⊢ ≤ ˙ = ≤ K
2 ltrnel.a ⊢ A = Atoms ⁡ K
3 ltrnel.h ⊢ H = LHyp ⁡ K
4 ltrnel.t ⊢ T = LTrn ⁡ K ⁡ W
5 simp1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → K ∈ HL ∧ W ∈ H
6 simp2r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → G ∈ T
7 eqid ⊢ Base K = Base K
8 7 3 4 ltrn1o ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T → G : Base K ⟶ 1-1 onto Base K
9 5 6 8 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → G : Base K ⟶ 1-1 onto Base K
10 f1of ⊢ G : Base K ⟶ 1-1 onto Base K → G : Base K ⟶ Base K
11 9 10 syl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → G : Base K ⟶ Base K
12 7 2 atbase ⊢ P ∈ A → P ∈ Base K
13 12 3ad2ant3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → P ∈ Base K
14 fvco3 ⊢ G : Base K ⟶ Base K ∧ P ∈ Base K → F ∘ G ⁡ P = F ⁡ G ⁡ P
15 11 13 14 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ G ∈ T ∧ P ∈ A → F ∘ G ⁡ P = F ⁡ G ⁡ P