cdleml5N

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	cdleml5N	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \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		simpl1	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \land V = \underset{˙}{0}) \to (K \in HL \land W \in H)$
8	1 2 3 5 6	tendo0cl	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} \in E$
9	7 8	syl	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \land V = \underset{˙}{0}) \to \underset{˙}{0} \in E$
10		simpl2l	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \land V = \underset{˙}{0}) \to U \in E$
11	1 2 3 5 6	tendo0mul	$⊢ ((K \in HL \land W \in H) \land U \in E) \to \underset{˙}{0} \circ U = \underset{˙}{0}$
12	7 10 11	syl2anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \land V = \underset{˙}{0}) \to \underset{˙}{0} \circ U = \underset{˙}{0}$
13		simpr	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \land V = \underset{˙}{0}) \to V = \underset{˙}{0}$
14	12 13	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \land V = \underset{˙}{0}) \to \underset{˙}{0} \circ U = V$
15		coeq1	$⊢ s = \underset{˙}{0} \to s \circ U = \underset{˙}{0} \circ U$
16	15	eqeq1d	$⊢ s = \underset{˙}{0} \to (s \circ U = V \leftrightarrow \underset{˙}{0} \circ U = V)$
17	16	rspcev	$⊢ (\underset{˙}{0} \in E \land \underset{˙}{0} \circ U = V) \to \exists s \in E s \circ U = V$
18	9 14 17	syl2anc	$⊢ (((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \land V = \underset{˙}{0}) \to \exists s \in E s \circ U = V$
19		simpl1	$⊢ (((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 (K \in HL \land W \in H)$
20		simpl2	$⊢ (((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 (U \in E \land V \in E)$
21		simpl3	$⊢ (((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 U \neq \underset{˙}{0}$
22		simpr	$⊢ (((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 V \neq \underset{˙}{0}$
23	1 2 3 4 5 6	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$
24	19 20 21 22 23	syl112anc	$⊢ (((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$
25	18 24	pm2.61dane	$⊢ ((K \in HL \land W \in H) \land (U \in E \land V \in E) \land U \neq \underset{˙}{0}) \to \exists s \in E s \circ U = V$

Metamath Proof Explorer

Theorem cdleml5N

Proof