cdleml1N

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cdleml1.b	$⊢ B = {Base}_{K}$
2		cdleml1.h	$⊢ H = LHyp (K)$
3		cdleml1.t	$⊢ T = LTrn (K) (W)$
4		cdleml1.r	$⊢ R = trL (K) (W)$
5		cdleml1.e	$⊢ E = TEndo (K) (W)$
6		simp1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to (K \in HL \land W \in H)$
7		simp21	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to U \in E$
8		simp23	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to f \in T$
9		eqid	$⊢ \leq_{K} = \leq_{K}$
10	9 2 3 4 5	tendotp	$⊢ ((K \in HL \land W \in H) \land U \in E \land f \in T) \to R (U (f)) \leq_{K} R (f)$
11	6 7 8 10	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (U (f)) \leq_{K} R (f)$
12		simp1l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to K \in HL$
13		hlatl	$⊢ K \in HL \to K \in AtLat$
14	12 13	syl	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to K \in AtLat$
15	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land f \in T) \to U (f) \in T$
16	6 7 8 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to U (f) \in T$
17		simp32	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to U (f) \neq {I ↾}_{B}$
18		eqid	$⊢ Atoms (K) = Atoms (K)$
19	1 18 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land U (f) \in T \land U (f) \neq {I ↾}_{B}) \to R (U (f)) \in Atoms (K)$
20	6 16 17 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (U (f)) \in Atoms (K)$
21		simp31	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to f \neq {I ↾}_{B}$
22	1 18 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land f \in T \land f \neq {I ↾}_{B}) \to R (f) \in Atoms (K)$
23	6 8 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (f) \in Atoms (K)$
24	9 18	atcmp	$⊢ (K \in AtLat \land R (U (f)) \in Atoms (K) \land R (f) \in Atoms (K)) \to (R (U (f)) \leq_{K} R (f) \leftrightarrow R (U (f)) = R (f))$
25	14 20 23 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to (R (U (f)) \leq_{K} R (f) \leftrightarrow R (U (f)) = R (f))$
26	11 25	mpbid	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (U (f)) = R (f)$
27		simp22	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to V \in E$
28	9 2 3 4 5	tendotp	$⊢ ((K \in HL \land W \in H) \land V \in E \land f \in T) \to R (V (f)) \leq_{K} R (f)$
29	6 27 8 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (V (f)) \leq_{K} R (f)$
30	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land f \in T) \to V (f) \in T$
31	6 27 8 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to V (f) \in T$
32		simp33	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to V (f) \neq {I ↾}_{B}$
33	1 18 2 3 4	trlnidat	$⊢ ((K \in HL \land W \in H) \land V (f) \in T \land V (f) \neq {I ↾}_{B}) \to R (V (f)) \in Atoms (K)$
34	6 31 32 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (V (f)) \in Atoms (K)$
35	9 18	atcmp	$⊢ (K \in AtLat \land R (V (f)) \in Atoms (K) \land R (f) \in Atoms (K)) \to (R (V (f)) \leq_{K} R (f) \leftrightarrow R (V (f)) = R (f))$
36	14 34 23 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to (R (V (f)) \leq_{K} R (f) \leftrightarrow R (V (f)) = R (f))$
37	29 36	mpbid	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (V (f)) = R (f)$
38	26 37	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E \land f \in T) \land (f \neq {I ↾}_{B} \land U (f) \neq {I ↾}_{B} \land V (f) \neq {I ↾}_{B})) \to R (U (f)) = R (V (f))$

Metamath Proof Explorer

Theorem cdleml1N

Proof