Metamath Proof Explorer

Theorem ltrncoelN

Description: Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel uses. (Contributed by NM, 1-May-2013) (New usage is discouraged.)

		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	ltrncoelN	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (G (P)) \in A \land \neg F (G (P)) \underset{˙}{\leq} W)$

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 \land \neg P \underset{˙}{\leq} W)) \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 \land \neg P \underset{˙}{\leq} W)) \to F \in T$
7	1 2 3 4	ltrnel	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
8	7	3adant2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
9	1 2 3 4	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)) \to (F (G (P)) \in A \land \neg F (G (P)) \underset{˙}{\leq} W)$
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 \land \neg P \underset{˙}{\leq} W)) \to (F (G (P)) \in A \land \neg F (G (P)) \underset{˙}{\leq} W)$