Metamath Proof Explorer

Theorem cdleml2N

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	cdleml2N	$⊢ ((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 \exists s \in E s (U (f)) = 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	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land f \in T) \to U (f) \in T$
10	6 7 8 9	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$
11		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$
12	2 3 5	tendocl	$⊢ ((K \in HL \land W \in H) \land V \in E \land f \in T) \to V (f) \in T$
13	6 11 8 12	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$
14	1 2 3 4 5	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))$
15	2 3 4 5	cdlemk	$⊢ ((K \in HL \land W \in H) \land (U (f) \in T \land V (f) \in T) \land R (U (f)) = R (V (f))) \to \exists s \in E s (U (f)) = V (f)$
16	6 10 13 14 15	syl121anc	$⊢ ((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 \exists s \in E s (U (f)) = V (f)$