cdlemj2

Description: Part of proof of Lemma J of Crawley p. 118. Eliminate p . (Contributed by NM, 20-Jun-2013)

	Ref	Expression
Hypotheses	cdlemj.b	$⊢ B = {Base}_{K}$
	cdlemj.h	$⊢ H = LHyp (K)$
	cdlemj.t	$⊢ T = LTrn (K) (W)$
	cdlemj.r	$⊢ R = trL (K) (W)$
	cdlemj.e	$⊢ E = TEndo (K) (W)$
Assertion	cdlemj2	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to U (h) = V (h)$

Proof

Step	Hyp	Ref	Expression
1		cdlemj.b	$⊢ B = {Base}_{K}$
2		cdlemj.h	$⊢ H = LHyp (K)$
3		cdlemj.t	$⊢ T = LTrn (K) (W)$
4		cdlemj.r	$⊢ R = trL (K) (W)$
5		cdlemj.e	$⊢ E = TEndo (K) (W)$
6		simpl1	$⊢ ((((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to ((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T))$
7		simpl2	$⊢ ((((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B})$
8		simpl3l	$⊢ ((((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to R (F) \neq R (g)$
9		simpl3r	$⊢ ((((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to R (g) \neq R (h)$
10		simpr	$⊢ ((((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to (p \in Atoms (K) \land \neg p \leq_{K} W)$
11		eqid	$⊢ \leq_{K} = \leq_{K}$
12		eqid	$⊢ Atoms (K) = Atoms (K)$
13	1 2 3 4 5 11 12	cdlemj1	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h) \land (p \in Atoms (K) \land \neg p \leq_{K} W))) \to U (h) (p) = V (h) (p)$
14	6 7 8 9 10 13	syl113anc	$⊢ ((((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \land (p \in Atoms (K) \land \neg p \leq_{K} W)) \to U (h) (p) = V (h) (p)$
15	14	exp32	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to (p \in Atoms (K) \to (\neg p \leq_{K} W \to U (h) (p) = V (h) (p)))$
16	15	ralrimiv	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to \forall p \in Atoms (K) (\neg p \leq_{K} W \to U (h) (p) = V (h) (p))$
17		simp11	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to (K \in HL \land W \in H)$
18		simp121	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to U \in E$
19		simp133	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to h \in T$
20	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land h \in T) \to U (h) \in T$
21	17 18 19 20	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to U (h) \in T$
22		simp122	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to V \in E$
23	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land h \in T) \to V (h) \in T$
24	17 22 19 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to V (h) \in T$
25	11 12 2 3	ltrneq	$⊢ ((K \in HL \land W \in H) \land U (h) \in T \land V (h) \in T) \to (\forall p \in Atoms (K) (\neg p \leq_{K} W \to U (h) (p) = V (h) (p)) \leftrightarrow U (h) = V (h))$
26	17 21 24 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to (\forall p \in Atoms (K) (\neg p \leq_{K} W \to U (h) (p) = V (h) (p)) \leftrightarrow U (h) = V (h))$
27	16 26	mpbid	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E \land U (F) = V (F)) \land (F \in T \land F \neq {I ↾}_{B} \land h \in T)) \land (h \neq {I ↾}_{B} \land g \in T \land g \neq {I ↾}_{B}) \land (R (F) \neq R (g) \land R (g) \neq R (h))) \to U (h) = V (h)$

Metamath Proof Explorer

Theorem cdlemj2

Proof