Metamath Proof Explorer

Theorem ltrncoat

Description: Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel , ltrnat uses. (Contributed by NM, 1-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	ltrncoat	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to F (G (P)) \in A$

Proof

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		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to F \in T$
7	1 2 3 4	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
8	7	3adant2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to G (P) \in A$
9	1 2 3 4	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land G (P) \in A) \to F (G (P)) \in A$
10	5 6 8 9	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land P \in A) \to F (G (P)) \in A$