cdlemg44b

Description: Eliminate ( FP ) =/= P , ( GP ) =/= P from cdlemg44a . (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	cdlemg44b	$⊢ ((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 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		simpl1	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to (K \in HL \land W \in H)$
7		simpl21	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to F \in T$
8		simpl23	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
9		simpl22	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to G \in T$
10	4 5 1 2	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)$
11	6 9 8 10	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 R (F) \neq R (G)) \land F (P) = P) \to (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)$
12		simpr	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to F (P) = P$
13	4 5 1 2	ltrnateq	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (G (P) \in A \land \neg G (P) \underset{˙}{\leq} W)) \land F (P) = P) \to F (G (P)) = G (P)$
14	6 7 8 11 12 13	syl131anc	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to F (G (P)) = G (P)$
15	12	fveq2d	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to G (F (P)) = G (P)$
16	14 15	eqtr4d	$⊢ (((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 R (F) \neq R (G)) \land F (P) = P) \to F (G (P)) = G (F (P))$
17		simpr	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to G (P) = P$
18	17	fveq2d	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to F (G (P)) = F (P)$
19		simpl1	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to (K \in HL \land W \in H)$
20		simpl22	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to G \in T$
21		simpl23	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
22		simpl21	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to F \in T$
23	4 5 1 2	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
24	19 22 21 23	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 R (F) \neq R (G)) \land G (P) = P) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
25	4 5 1 2	ltrnateq	$⊢ ((K \in HL \land W \in H) \land (G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \land G (P) = P) \to G (F (P)) = F (P)$
26	19 20 21 24 17 25	syl131anc	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to G (F (P)) = F (P)$
27	18 26	eqtr4d	$⊢ (((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 R (F) \neq R (G)) \land G (P) = P) \to F (G (P)) = G (F (P))$
28		simpl1	$⊢ (((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 R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (K \in HL \land W \in H)$
29		simpl2	$⊢ (((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 R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to (F \in T \land G \in T \land (P \in A \land \neg P \underset{˙}{\leq} W))$
30		simprl	$⊢ (((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 R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to F (P) \neq P$
31		simprr	$⊢ (((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 R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to G (P) \neq P$
32		simpl3	$⊢ (((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 R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to R (F) \neq R (G)$
33	1 2 3 4 5	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))$
34	28 29 30 31 32 33	syl113anc	$⊢ (((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 R (F) \neq R (G)) \land (F (P) \neq P \land G (P) \neq P)) \to F (G (P)) = G (F (P))$
35	16 27 34	pm2.61da2ne	$⊢ ((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 R (F) \neq R (G)) \to F (G (P)) = G (F (P))$

Metamath Proof Explorer

Theorem cdlemg44b

Proof