cdlemg44

Description: Part of proof of Lemma G of Crawley p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg44.h	$⊢ H = LHyp (K)$
2		cdlemg44.t	$⊢ T = LTrn (K) (W)$
3		cdlemg44.r	$⊢ R = trL (K) (W)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	4 5 1	lhpexnle	$⊢ (K \in HL \land W \in H) \to \exists p \in Atoms (K) \neg p \leq_{K} W$
7	6	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to \exists p \in Atoms (K) \neg p \leq_{K} W$
8		simp11	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to (K \in HL \land W \in H)$
9		simp12l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to F \in T$
10		simp12r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to G \in T$
11	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
12	8 9 10 11	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to F \circ G \in T$
13	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F \in T) \to G \circ F \in T$
14	8 10 9 13	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to G \circ F \in T$
15		3simpc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to (p \in Atoms (K) \land \neg p \leq_{K} W)$
16		simp13	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to R (F) \neq R (G)$
17	1 2 3 4 5	cdlemg44b	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \land R (F) \neq R (G)) \to F (G (p)) = G (F (p))$
18	8 9 10 15 16 17	syl131anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to F (G (p)) = G (F (p))$
19		simp12	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to (F \in T \land G \in T)$
20		simp2	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to p \in Atoms (K)$
21	4 5 1 2	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land p \in Atoms (K)) \to (F \circ G) (p) = F (G (p))$
22	8 19 20 21	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to (F \circ G) (p) = F (G (p))$
23	4 5 1 2	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F \in T) \land p \in Atoms (K)) \to (G \circ F) (p) = G (F (p))$
24	8 10 9 20 23	syl121anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to (G \circ F) (p) = G (F (p))$
25	18 22 24	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to (F \circ G) (p) = (G \circ F) (p)$
26	4 5 1 2	cdlemd	$⊢ (((K \in HL \land W \in H) \land F \circ G \in T \land G \circ F \in T) \land (p \in Atoms (K) \land \neg p \leq_{K} W) \land (F \circ G) (p) = (G \circ F) (p)) \to F \circ G = G \circ F$
27	8 12 14 15 25 26	syl311anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \land p \in Atoms (K) \land \neg p \leq_{K} W) \to F \circ G = G \circ F$
28	27	rexlimdv3a	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to (\exists p \in Atoms (K) \neg p \leq_{K} W \to F \circ G = G \circ F)$
29	7 28	mpd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land R (F) \neq R (G)) \to F \circ G = G \circ F$

Metamath Proof Explorer

Theorem cdlemg44

Proof