ltrncoval

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

	Ref	Expression
Hypotheses	ltrnel.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrnel.a	$⊢ A = Atoms (K)$
	ltrnel.h	$⊢ H = LHyp (K)$
	ltrnel.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to (F \circ G) (P) = F (G (P))$

Step	Hyp	Ref	Expression
1		ltrnel.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrnel.a	$⊢ A = Atoms (K)$
3		ltrnel.h	$⊢ H = LHyp (K)$
4		ltrnel.t	$⊢ T = LTrn (K) (W)$
5		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to (K \in HL \land W \in H)$
6		simp2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to G \in T$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 3 4	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
9	5 6 8	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
10		f1of	$⊢ G : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \to G : {Base}_{K} ⟶ {Base}_{K}$
11	9 10	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to G : {Base}_{K} ⟶ {Base}_{K}$
12	7 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
13	12	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to P \in {Base}_{K}$
14		fvco3	$⊢ (G : {Base}_{K} ⟶ {Base}_{K} \land P \in {Base}_{K}) \to (F \circ G) (P) = F (G (P))$
15	11 13 14	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to (F \circ G) (P) = F (G (P))$

Metamath Proof Explorer