cdleml9

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013)

	Ref	Expression
Hypotheses	cdleml6.b	$⊢ B = {Base}_{K}$
	cdleml6.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleml6.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleml6.h	$⊢ H = LHyp (K)$
	cdleml6.t	$⊢ T = LTrn (K) (W)$
	cdleml6.r	$⊢ R = trL (K) (W)$
	cdleml6.p	$⊢ Q = oc (K) (W)$
	cdleml6.z	$⊢ Z = (Q \underset{˙}{\lor} R (b)) \underset{˙}{\land} (h (Q) \underset{˙}{\lor} R (b \circ {s (h)}^{-1}))$
	cdleml6.y	$⊢ Y = (Q \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
	cdleml6.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (s (h)) \land R (b) \neq R (g)) \to z (Q) = Y))$
	cdleml6.u	$⊢ U = (g \in T ⟼ if (s (h) = h, g, X))$
	cdleml6.e	$⊢ E = TEndo (K) (W)$
	cdleml6.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
Assertion	cdleml9	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to U \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		cdleml6.b	$⊢ B = {Base}_{K}$
2		cdleml6.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleml6.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleml6.h	$⊢ H = LHyp (K)$
5		cdleml6.t	$⊢ T = LTrn (K) (W)$
6		cdleml6.r	$⊢ R = trL (K) (W)$
7		cdleml6.p	$⊢ Q = oc (K) (W)$
8		cdleml6.z	$⊢ Z = (Q \underset{˙}{\lor} R (b)) \underset{˙}{\land} (h (Q) \underset{˙}{\lor} R (b \circ {s (h)}^{-1}))$
9		cdleml6.y	$⊢ Y = (Q \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
10		cdleml6.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (s (h)) \land R (b) \neq R (g)) \to z (Q) = Y))$
11		cdleml6.u	$⊢ U = (g \in T ⟼ if (s (h) = h, g, X))$
12		cdleml6.e	$⊢ E = TEndo (K) (W)$
13		cdleml6.o	$⊢ \underset{˙}{0} = (f \in T ⟼ {I ↾}_{B})$
14	1 4 5 12 13	tendo1ne0	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq \underset{˙}{0}$
15	14	3ad2ant1	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to {I ↾}_{T} \neq \underset{˙}{0}$
16	1 2 3 4 5 6 7 8 9 10 11 12 13	cdleml8	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to U \circ s = {I ↾}_{T}$
17	16	adantr	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \land U = \underset{˙}{0}) \to U \circ s = {I ↾}_{T}$
18		coeq1	$⊢ U = \underset{˙}{0} \to U \circ s = \underset{˙}{0} \circ s$
19		simp1	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to (K \in HL \land W \in H)$
20		simp3l	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to s \in E$
21	1 4 5 12 13	tendo0mul	$⊢ ((K \in HL \land W \in H) \land s \in E) \to \underset{˙}{0} \circ s = \underset{˙}{0}$
22	19 20 21	syl2anc	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to \underset{˙}{0} \circ s = \underset{˙}{0}$
23	18 22	sylan9eqr	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \land U = \underset{˙}{0}) \to U \circ s = \underset{˙}{0}$
24	17 23	eqtr3d	$⊢ (((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \land U = \underset{˙}{0}) \to {I ↾}_{T} = \underset{˙}{0}$
25	24	ex	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to (U = \underset{˙}{0} \to {I ↾}_{T} = \underset{˙}{0})$
26	25	necon3d	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to ({I ↾}_{T} \neq \underset{˙}{0} \to U \neq \underset{˙}{0})$
27	15 26	mpd	$⊢ ((K \in HL \land W \in H) \land (h \in T \land h \neq {I ↾}_{B}) \land (s \in E \land s \neq \underset{˙}{0})) \to U \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem cdleml9

Proof