cdleml3N

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	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$

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		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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to (K \in HL \land W \in H)$
8		simp2	$⊢ ((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 (U \in E \land V \in E \land f \in T)$
9		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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to f \neq {I ↾}_{B}$
10		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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to U \neq \underset{˙}{0}$
11		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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to U \in E$
12		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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to f \in T$
13	1 2 3 5 6	tendoid0	$⊢ ((K \in HL \land W \in H) \land U \in E \land (f \in T \land f \neq {I ↾}_{B})) \to (U (f) = {I ↾}_{B} \leftrightarrow U = \underset{˙}{0})$
14	7 11 12 9 13	syl112anc	$⊢ ((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 (U (f) = {I ↾}_{B} \leftrightarrow U = \underset{˙}{0})$
15	14	necon3bid	$⊢ ((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 (U (f) \neq {I ↾}_{B} \leftrightarrow U \neq \underset{˙}{0})$
16	10 15	mpbird	$⊢ ((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 U (f) \neq {I ↾}_{B}$
17		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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to V \neq \underset{˙}{0}$
18		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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \to V \in E$
19	1 2 3 5 6	tendoid0	$⊢ ((K \in HL \land W \in H) \land V \in E \land (f \in T \land f \neq {I ↾}_{B})) \to (V (f) = {I ↾}_{B} \leftrightarrow V = \underset{˙}{0})$
20	7 18 12 9 19	syl112anc	$⊢ ((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 (V (f) = {I ↾}_{B} \leftrightarrow V = \underset{˙}{0})$
21	20	necon3bid	$⊢ ((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 (V (f) \neq {I ↾}_{B} \leftrightarrow V \neq \underset{˙}{0})$
22	17 21	mpbird	$⊢ ((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 V (f) \neq {I ↾}_{B}$
23	1 2 3 4 5	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)$
24	7 8 9 16 22 23	syl113anc	$⊢ ((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 (U (f)) = V (f)$
25		simpl1	$⊢ (((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})) \land s \in E) \to (K \in HL \land W \in H)$
26		simpr	$⊢ (((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})) \land s \in E) \to s \in E$
27		simpl21	$⊢ (((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})) \land s \in E) \to U \in E$
28		simpl23	$⊢ (((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})) \land s \in E) \to f \in T$
29	2 3 5	tendocoval	$⊢ ((K \in HL \land W \in H) \land (s \in E \land U \in E) \land f \in T) \to (s \circ U) (f) = s (U (f))$
30	25 26 27 28 29	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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land s \in E) \to (s \circ U) (f) = s (U (f))$
31	30	eqeq1d	$⊢ (((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})) \land s \in E) \to ((s \circ U) (f) = V (f) \leftrightarrow s (U (f)) = V (f))$
32		simp11	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to (K \in HL \land W \in H)$
33		simp2	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to s \in E$
34		simp121	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to U \in E$
35	2 5	tendococl	$⊢ ((K \in HL \land W \in H) \land s \in E \land U \in E) \to s \circ U \in E$
36	32 33 34 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 \neq \underset{˙}{0} \land V \neq \underset{˙}{0})) \land s \in E \land (s \circ U) (f) = V (f)) \to s \circ U \in E$
37		simp122	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to V \in E$
38		simp3	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to (s \circ U) (f) = V (f)$
39		simp123	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to f \in T$
40		simp131	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to f \neq {I ↾}_{B}$
41	1 2 3 5	tendocan	$⊢ ((K \in HL \land W \in H) \land (s \circ U \in E \land V \in E \land (s \circ U) (f) = V (f)) \land (f \in T \land f \neq {I ↾}_{B})) \to s \circ U = V$
42	32 36 37 38 39 40 41	syl132anc	$⊢ (((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})) \land s \in E \land (s \circ U) (f) = V (f)) \to s \circ U = V$
43	42	3expia	$⊢ (((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})) \land s \in E) \to ((s \circ U) (f) = V (f) \to s \circ U = V)$
44	31 43	sylbird	$⊢ (((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})) \land s \in E) \to (s (U (f)) = V (f) \to s \circ U = V)$
45	44	reximdva	$⊢ ((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 (U (f)) = V (f) \to \exists s \in E s \circ U = V)$
46	24 45	mpd	$⊢ ((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$

Metamath Proof Explorer

Theorem cdleml3N

Proof