cdlemj3

Description: Part of proof of Lemma J of Crawley p. 118. Eliminate g . (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	cdlemj3	$⊢ (((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}) \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}) \to (K \in HL \land W \in H)$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8		eqid	$⊢ Atoms (K) = Atoms (K)$
9	7 8 2	lhpexle2	$⊢ (K \in HL \land W \in H) \to \exists u \in Atoms (K) (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))$
10	6 9	syl	$⊢ (((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}) \to \exists u \in Atoms (K) (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))$
11		simpl1l	$⊢ (((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}) \to K \in HL$
12	11	adantr	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to K \in HL$
13		simpl1r	$⊢ (((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}) \to W \in H$
14	13	adantr	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to W \in H$
15		simprl	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to u \in Atoms (K)$
16		simprr1	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to u \leq_{K} W$
17	1 7 8 2 3 4	cdlemfnid	$⊢ ((K \in HL \land W \in H) \land (u \in Atoms (K) \land u \leq_{K} W)) \to \exists g \in T (R (g) = u \land g \neq {I ↾}_{B})$
18	12 14 15 16 17	syl22anc	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to \exists g \in T (R (g) = u \land g \neq {I ↾}_{B})$
19		simp1l	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \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))$
20		simp1r	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to h \neq {I ↾}_{B}$
21		simp3l	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to g \in T$
22		simp3rr	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to g \neq {I ↾}_{B}$
23		simp2r2	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to u \neq R (F)$
24	23	necomd	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to R (F) \neq u$
25		simp3rl	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to R (g) = u$
26	24 25	neeqtrrd	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to R (F) \neq R (g)$
27		simp2r3	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to u \neq R (h)$
28	25 27	eqnetrd	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to R (g) \neq R (h)$
29	1 2 3 4 5	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)$
30	19 20 21 22 26 28 29	syl132anc	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h))) \land (g \in T \land (R (g) = u \land g \neq {I ↾}_{B}))) \to U (h) = V (h)$
31	30	3expia	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to ((g \in T \land (R (g) = u \land g \neq {I ↾}_{B})) \to U (h) = V (h))$
32	31	expd	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to (g \in T \to ((R (g) = u \land g \neq {I ↾}_{B}) \to U (h) = V (h)))$
33	32	rexlimdv	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to (\exists g \in T (R (g) = u \land g \neq {I ↾}_{B}) \to U (h) = V (h))$
34	18 33	mpd	$⊢ ((((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 (u \in Atoms (K) \land (u \leq_{K} W \land u \neq R (F) \land u \neq R (h)))) \to U (h) = V (h)$
35	10 34	rexlimddv	$⊢ (((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}) \to U (h) = V (h)$

Metamath Proof Explorer

Theorem cdlemj3

Proof