Metamath Proof Explorer

Theorem trlco

Description: The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of Crawley p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013)

		Ref	Expression
	Hypotheses	trlco.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		trlco.j	$⊢ \underset{˙}{\lor} = join (K)$
		trlco.h	$⊢ H = LHyp (K)$
		trlco.t	$⊢ T = LTrn (K) (W)$
		trlco.r	$⊢ R = trL (K) (W)$
	Assertion	trlco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G))$

Proof

Step	Hyp	Ref	Expression
1		trlco.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trlco.j	$⊢ \underset{˙}{\lor} = join (K)$
3		trlco.h	$⊢ H = LHyp (K)$
4		trlco.t	$⊢ T = LTrn (K) (W)$
5		trlco.r	$⊢ R = trL (K) (W)$
6		eqid	$⊢ Atoms (K) = Atoms (K)$
7	1 6 3	lhpexnle	$⊢ (K \in HL \land W \in H) \to \exists p \in Atoms (K) \neg p \underset{˙}{\leq} W$
8	7	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to \exists p \in Atoms (K) \neg p \underset{˙}{\leq} W$
9		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
10		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)) \to F \in T$
11		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)) \to G \in T$
12		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)) \to (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)$
13		eqid	$⊢ meet (K) = meet (K)$
14	1 2 3 4 5 13 6	trlcolem	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)) \to R (F \circ G) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G))$
15	9 10 11 12 14	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land \neg p \underset{˙}{\leq} W)) \to R (F \circ G) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G))$
16	8 15	rexlimddv	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to R (F \circ G) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G))$