cdlemg4a

Description: TODO: FIX COMMENT If fg(p) = p, then tr f = tr g. (Contributed by NM, 23-Apr-2013)

	Ref	Expression
Hypotheses	cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg4.a	$⊢ A = Atoms (K)$
	cdlemg4.h	$⊢ H = LHyp (K)$
	cdlemg4.t	$⊢ T = LTrn (K) (W)$
	cdlemg4.r	$⊢ R = trL (K) (W)$
Assertion	cdlemg4a	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to R (F) = R (G)$

Proof

Step	Hyp	Ref	Expression
1		cdlemg4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg4.a	$⊢ A = Atoms (K)$
3		cdlemg4.h	$⊢ H = LHyp (K)$
4		cdlemg4.t	$⊢ T = LTrn (K) (W)$
5		cdlemg4.r	$⊢ R = trL (K) (W)$
6		simp3	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to F (G (P)) = P$
7	6	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to G (P) join (K) F (G (P)) = G (P) join (K) P$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to K \in HL$
9		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to (K \in HL \land W \in H)$
10		simp23	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to G \in T$
11		simp21	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
12	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)$
13	12	simpld	$⊢ ((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$
14	9 10 11 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to G (P) \in A$
15		simp21l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to P \in A$
16		eqid	$⊢ join (K) = join (K)$
17	16 2	hlatjcom	$⊢ (K \in HL \land G (P) \in A \land P \in A) \to G (P) join (K) P = P join (K) G (P)$
18	8 14 15 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to G (P) join (K) P = P join (K) G (P)$
19	7 18	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to G (P) join (K) F (G (P)) = P join (K) G (P)$
20	19	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to (G (P) join (K) F (G (P))) meet (K) W = (P join (K) G (P)) meet (K) W$
21		simp22	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to F \in T$
22	9 10 11 12	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
23		eqid	$⊢ meet (K) = meet (K)$
24	1 16 23 2 3 4 5	trlval2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)) \to R (F) = (G (P) join (K) F (G (P))) meet (K) W$
25	9 21 22 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to R (F) = (G (P) join (K) F (G (P))) meet (K) W$
26	1 16 23 2 3 4 5	trlval2	$⊢ ((K \in HL \land W \in H) \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (G) = (P join (K) G (P)) meet (K) W$
27	9 10 11 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to R (G) = (P join (K) G (P)) meet (K) W$
28	20 25 27	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land F \in T \land G \in T) \land F (G (P)) = P) \to R (F) = R (G)$

Metamath Proof Explorer

Theorem cdlemg4a

Proof