tendoex

Description: Generalization of Lemma K of Crawley p. 118, cdlemk . TODO: can this be used to shorten uses of cdlemk ? (Contributed by NM, 15-Oct-2013)

	Ref	Expression
Hypotheses	tendoex.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	tendoex.h	$⊢ H = LHyp (K)$
	tendoex.t	$⊢ T = LTrn (K) (W)$
	tendoex.r	$⊢ R = trL (K) (W)$
	tendoex.e	$⊢ E = TEndo (K) (W)$
Assertion	tendoex	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to \exists u \in E u (F) = N$

Proof

Step	Hyp	Ref	Expression
1		tendoex.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		tendoex.h	$⊢ H = LHyp (K)$
3		tendoex.t	$⊢ T = LTrn (K) (W)$
4		tendoex.r	$⊢ R = trL (K) (W)$
5		tendoex.e	$⊢ E = TEndo (K) (W)$
6		simpl1l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to K \in HL$
7		hlop	$⊢ K \in HL \to K \in OP$
8	6 7	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to K \in OP$
9		simpl1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to (K \in HL \land W \in H)$
10		simpl2r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to N \in T$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 2 3 4	trlcl	$⊢ ((K \in HL \land W \in H) \land N \in T) \to R (N) \in {Base}_{K}$
13	9 10 12	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to R (N) \in {Base}_{K}$
14		simpr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to R (F) \in Atoms (K)$
15		simpl3	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to R (N) \underset{˙}{\leq} R (F)$
16		eqid	$⊢ 0. (K) = 0. (K)$
17		eqid	$⊢ Atoms (K) = Atoms (K)$
18	11 1 16 17	leat	$⊢ ((K \in OP \land R (N) \in {Base}_{K} \land R (F) \in Atoms (K)) \land R (N) \underset{˙}{\leq} R (F)) \to (R (N) = R (F) \lor R (N) = 0. (K))$
19	8 13 14 15 18	syl31anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) \in Atoms (K)) \to (R (N) = R (F) \lor R (N) = 0. (K))$
20		simp3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to R (N) \underset{˙}{\leq} R (F)$
21		breq2	$⊢ R (F) = 0. (K) \to (R (N) \underset{˙}{\leq} R (F) \leftrightarrow R (N) \underset{˙}{\leq} 0. (K))$
22	20 21	syl5ibcom	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to (R (F) = 0. (K) \to R (N) \underset{˙}{\leq} 0. (K))$
23	22	imp	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to R (N) \underset{˙}{\leq} 0. (K)$
24		simpl1l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to K \in HL$
25	24 7	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to K \in OP$
26		simpl1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to (K \in HL \land W \in H)$
27		simpl2r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to N \in T$
28	26 27 12	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to R (N) \in {Base}_{K}$
29	11 1 16	ople0	$⊢ (K \in OP \land R (N) \in {Base}_{K}) \to (R (N) \underset{˙}{\leq} 0. (K) \leftrightarrow R (N) = 0. (K))$
30	25 28 29	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to (R (N) \underset{˙}{\leq} 0. (K) \leftrightarrow R (N) = 0. (K))$
31	23 30	mpbid	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to R (N) = 0. (K)$
32	31	olcd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \land R (F) = 0. (K)) \to (R (N) = R (F) \lor R (N) = 0. (K))$
33		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to (K \in HL \land W \in H)$
34		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to F \in T$
35	16 17 2 3 4	trlator0	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in Atoms (K) \lor R (F) = 0. (K))$
36	33 34 35	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to (R (F) \in Atoms (K) \lor R (F) = 0. (K))$
37	19 32 36	mpjaodan	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to (R (N) = R (F) \lor R (N) = 0. (K))$
38	37	3expa	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) \underset{˙}{\leq} R (F)) \to (R (N) = R (F) \lor R (N) = 0. (K))$
39		eqcom	$⊢ R (N) = R (F) \leftrightarrow R (F) = R (N)$
40	2 3 4 5	cdlemk	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (F) = R (N)) \to \exists u \in E u (F) = N$
41	40	3expa	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (F) = R (N)) \to \exists u \in E u (F) = N$
42	39 41	sylan2b	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) = R (F)) \to \exists u \in E u (F) = N$
43		eqid	$⊢ (h \in T ⟼ {I ↾}_{{Base}_{K}}) = (h \in T ⟼ {I ↾}_{{Base}_{K}})$
44	11 2 3 5 43	tendo0cl	$⊢ (K \in HL \land W \in H) \to (h \in T ⟼ {I ↾}_{{Base}_{K}}) \in E$
45	44	ad2antrr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) = 0. (K)) \to (h \in T ⟼ {I ↾}_{{Base}_{K}}) \in E$
46		simplrl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) = 0. (K)) \to F \in T$
47	43 11	tendo02	$⊢ F \in T \to (h \in T ⟼ {I ↾}_{{Base}_{K}}) (F) = {I ↾}_{{Base}_{K}}$
48	46 47	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) = 0. (K)) \to (h \in T ⟼ {I ↾}_{{Base}_{K}}) (F) = {I ↾}_{{Base}_{K}}$
49	11 16 2 3 4	trlid0b	$⊢ ((K \in HL \land W \in H) \land N \in T) \to (N = {I ↾}_{{Base}_{K}} \leftrightarrow R (N) = 0. (K))$
50	49	adantrl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T)) \to (N = {I ↾}_{{Base}_{K}} \leftrightarrow R (N) = 0. (K))$
51	50	biimpar	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) = 0. (K)) \to N = {I ↾}_{{Base}_{K}}$
52	48 51	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) = 0. (K)) \to (h \in T ⟼ {I ↾}_{{Base}_{K}}) (F) = N$
53		fveq1	$⊢ u = (h \in T ⟼ {I ↾}_{{Base}_{K}}) \to u (F) = (h \in T ⟼ {I ↾}_{{Base}_{K}}) (F)$
54	53	eqeq1d	$⊢ u = (h \in T ⟼ {I ↾}_{{Base}_{K}}) \to (u (F) = N \leftrightarrow (h \in T ⟼ {I ↾}_{{Base}_{K}}) (F) = N)$
55	54	rspcev	$⊢ ((h \in T ⟼ {I ↾}_{{Base}_{K}}) \in E \land (h \in T ⟼ {I ↾}_{{Base}_{K}}) (F) = N) \to \exists u \in E u (F) = N$
56	45 52 55	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) = 0. (K)) \to \exists u \in E u (F) = N$
57	42 56	jaodan	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land (R (N) = R (F) \lor R (N) = 0. (K))) \to \exists u \in E u (F) = N$
58	38 57	syldan	$⊢ (((K \in HL \land W \in H) \land (F \in T \land N \in T)) \land R (N) \underset{˙}{\leq} R (F)) \to \exists u \in E u (F) = N$
59	58	3impa	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T) \land R (N) \underset{˙}{\leq} R (F)) \to \exists u \in E u (F) = N$

Metamath Proof Explorer

Theorem tendoex

Proof