ltrnco

Description: The composition of two translations is a translation. Part of proof of Lemma G of Crawley p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013)

	Ref	Expression
Hypotheses	ltrnco.h	$⊢ H = LHyp (K)$
	ltrnco.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$

Proof

Step	Hyp	Ref	Expression
1		ltrnco.h	$⊢ H = LHyp (K)$
2		ltrnco.t	$⊢ T = LTrn (K) (W)$
3		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (K \in HL \land W \in H)$
4		eqid	$⊢ LDil (K) (W) = LDil (K) (W)$
5	1 4 2	ltrnldil	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in LDil (K) (W)$
6	5	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \in LDil (K) (W)$
7	1 4 2	ltrnldil	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G \in LDil (K) (W)$
8	7	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to G \in LDil (K) (W)$
9	1 4	ldilco	$⊢ ((K \in HL \land W \in H) \land F \in LDil (K) (W) \land G \in LDil (K) (W)) \to F \circ G \in LDil (K) (W)$
10	3 6 8 9	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in LDil (K) (W)$
11		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (K \in HL \land W \in H)$
12		simp2l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to p \in Atoms (K)$
13		simp3l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to \neg p \leq_{K} W$
14	12 13	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (p \in Atoms (K) \land \neg p \leq_{K} W)$
15		simp2r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to q \in Atoms (K)$
16		simp3r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to \neg q \leq_{K} W$
17	15 16	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (q \in Atoms (K) \land \neg q \leq_{K} W)$
18		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to F \in T$
19		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to G \in T$
20		eqid	$⊢ \leq_{K} = \leq_{K}$
21		eqid	$⊢ join (K) = join (K)$
22		eqid	$⊢ meet (K) = meet (K)$
23		eqid	$⊢ Atoms (K) = Atoms (K)$
24	20 21 22 23 1 2	cdlemg41	$⊢ ((K \in HL \land W \in H) \land ((p \in Atoms (K) \land \neg p \leq_{K} W) \land (q \in Atoms (K) \land \neg q \leq_{K} W)) \land (F \in T \land G \in T)) \to (p join (K) (F \circ G) (p)) meet (K) W = (q join (K) (F \circ G) (q)) meet (K) W$
25	11 14 17 18 19 24	syl122anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (p \in Atoms (K) \land q \in Atoms (K)) \land (\neg p \leq_{K} W \land \neg q \leq_{K} W)) \to (p join (K) (F \circ G) (p)) meet (K) W = (q join (K) (F \circ G) (q)) meet (K) W$
26	25	3exp	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to ((p \in Atoms (K) \land q \in Atoms (K)) \to ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) (F \circ G) (p)) meet (K) W = (q join (K) (F \circ G) (q)) meet (K) W))$
27	26	ralrimivv	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to \forall p \in Atoms (K) \forall q \in Atoms (K) ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) (F \circ G) (p)) meet (K) W = (q join (K) (F \circ G) (q)) meet (K) W)$
28	20 21 22 23 1 4 2	isltrn	$⊢ (K \in HL \land W \in H) \to (F \circ G \in T \leftrightarrow (F \circ G \in LDil (K) (W) \land \forall p \in Atoms (K) \forall q \in Atoms (K) ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) (F \circ G) (p)) meet (K) W = (q join (K) (F \circ G) (q)) meet (K) W)))$
29	28	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to (F \circ G \in T \leftrightarrow (F \circ G \in LDil (K) (W) \land \forall p \in Atoms (K) \forall q \in Atoms (K) ((\neg p \leq_{K} W \land \neg q \leq_{K} W) \to (p join (K) (F \circ G) (p)) meet (K) W = (q join (K) (F \circ G) (q)) meet (K) W)))$
30	10 27 29	mpbir2and	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$

Metamath Proof Explorer

Theorem ltrnco

Proof