Metamath Proof Explorer

Theorem cdleml4N

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)$
		cdleml3.o	$⊢ \underset{˙}{0} = (g \in T ⟼ {I ↾}_{B})$
	Assertion	cdleml4N	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to \exists s \in E s \circ U = V$

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		cdleml3.o	$⊢ \underset{˙}{0} = (g \in T ⟼ {I ↾}_{B})$
7	1 2 3	cdlemftr0	$⊢ (K \in HL \land W \in H) \to \exists f \in T f \neq {I ↾}_{B}$
8	7	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to \exists f \in T f \neq {I ↾}_{B}$
9		simp11	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to (K \in HL \land W \in H)$
10		simp12l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to U \in E$
11		simp12r	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to V \in E$
12		simp2	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to f \in T$
13		simp3	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to f \neq {I ↾}_{B}$
14		simp13l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to U \neq \underset{˙}{0}$
15		simp13r	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to V \neq \underset{˙}{0}$
16	1 2 3 4 5 6	cdleml3N	$⊢ ((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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to \exists s \in E s \circ U = V$
17	9 10 11 12 13 14 15 16	syl133anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land f \in T \land f \neq {I ↾}_{B}) \to \exists s \in E s \circ U = V$
18	17	rexlimdv3a	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to (\exists f \in T f \neq {I ↾}_{B} \to \exists s \in E s \circ U = V)$
19	8 18	mpd	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land (U \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to \exists s \in E s \circ U = V$