cdlemg44a

Description: Part of proof of Lemma G of Crawley p. 116, fourth line of third paragraph on p. 117: "so fg(p) = gf(p)." (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)$
	cdlemg44.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg44.a	$⊢ A = Atoms (K)$
Assertion	cdlemg44a	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F (G (P)) = G (F (P))$

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		cdlemg44.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
5		cdlemg44.a	$⊢ A = Atoms (K)$
6		simp1l	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to K \in HL$
7	6	hllatd	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to K \in Lat$
8		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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to (K \in HL \land W \in H)$
9		simp22	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to G \in T$
10		simp23l	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to P \in A$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 5	atbase	$⊢ P \in A \to P \in {Base}_{K}$
13	10 12	syl	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to P \in {Base}_{K}$
14	11 1 2	ltrncl	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in {Base}_{K}) \to G (P) \in {Base}_{K}$
15	8 9 13 14	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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to G (P) \in {Base}_{K}$
16		simp21	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F \in T$
17	11 1 2 3	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
18	8 16 17	syl2anc	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to R (F) \in {Base}_{K}$
19		eqid	$⊢ join (K) = join (K)$
20	11 19	latjcl	$⊢ (K \in Lat \land G (P) \in {Base}_{K} \land R (F) \in {Base}_{K}) \to G (P) join (K) R (F) \in {Base}_{K}$
21	7 15 18 20	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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to G (P) join (K) R (F) \in {Base}_{K}$
22	11 1 2	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in {Base}_{K}) \to F (P) \in {Base}_{K}$
23	8 16 13 22	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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F (P) \in {Base}_{K}$
24	11 1 2 3	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
25	8 9 24	syl2anc	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to R (G) \in {Base}_{K}$
26	11 19	latjcl	$⊢ (K \in Lat \land F (P) \in {Base}_{K} \land R (G) \in {Base}_{K}) \to F (P) join (K) R (G) \in {Base}_{K}$
27	7 23 25 26	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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F (P) join (K) R (G) \in {Base}_{K}$
28		eqid	$⊢ meet (K) = meet (K)$
29	11 28	latmcom	$⊢ (K \in Lat \land G (P) join (K) R (F) \in {Base}_{K} \land F (P) join (K) R (G) \in {Base}_{K}) \to (G (P) join (K) R (F)) meet (K) (F (P) join (K) R (G)) = (F (P) join (K) R (G)) meet (K) (G (P) join (K) R (F))$
30	7 21 27 29	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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to (G (P) join (K) R (F)) meet (K) (F (P) join (K) R (G)) = (F (P) join (K) R (G)) meet (K) (G (P) join (K) R (F))$
31		simp23	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
32		simp32	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to G (P) \neq P$
33		simp33	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to R (F) \neq R (G)$
34	4 19 5 1 2 3 28	cdlemg43	$⊢ ((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) \land G (P) \neq P \land R (F) \neq R (G))) \to F (G (P)) = (G (P) join (K) R (F)) meet (K) (F (P) join (K) R (G))$
35	8 16 9 31 32 33 34	syl123anc	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F (G (P)) = (G (P) join (K) R (F)) meet (K) (F (P) join (K) R (G))$
36		simp31	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F (P) \neq P$
37	33	necomd	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to R (G) \neq R (F)$
38	4 19 5 1 2 3 28	cdlemg43	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F (P) \neq P \land R (G) \neq R (F))) \to G (F (P)) = (F (P) join (K) R (G)) meet (K) (G (P) join (K) R (F))$
39	8 9 16 31 36 37 38	syl123anc	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to G (F (P)) = (F (P) join (K) R (G)) meet (K) (G (P) join (K) R (F))$
40	30 35 39	3eqtr4d	$⊢ ((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)) \land (F (P) \neq P \land G (P) \neq P \land R (F) \neq R (G))) \to F (G (P)) = G (F (P))$

Metamath Proof Explorer

Theorem cdlemg44a

Proof