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 = ( le ‘ 𝐾 )
ltrnel.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrnel.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnel.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrncoval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → ( ( 𝐹𝐺 ) ‘ 𝑃 ) = ( 𝐹 ‘ ( 𝐺𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 ltrnel.l = ( le ‘ 𝐾 )
2 ltrnel.a 𝐴 = ( Atoms ‘ 𝐾 )
3 ltrnel.h 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrnel.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → 𝐺𝑇 )
7 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 3 4 ltrn1o ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
9 5 6 8 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) )
10 f1of ( 𝐺 : ( Base ‘ 𝐾 ) –1-1-onto→ ( Base ‘ 𝐾 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
11 9 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) )
12 7 2 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
13 12 3ad2ant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
14 fvco3 ( ( 𝐺 : ( Base ‘ 𝐾 ) ⟶ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑃 ) = ( 𝐹 ‘ ( 𝐺𝑃 ) ) )
15 11 13 14 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐺𝑇 ) ∧ 𝑃𝐴 ) → ( ( 𝐹𝐺 ) ‘ 𝑃 ) = ( 𝐹 ‘ ( 𝐺𝑃 ) ) )