cdleml6

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	cdleml6	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to (U \in E \land U (s (h)) = h)$

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		simp1	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to (K \in HL \land W \in H)$
15		simp3l	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to s \in E$
16		simp2	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to h \in T$
17	4 5 12	tendocl	$⊢ ((K \in HL \land W \in H) \land s \in E \land h \in T) \to s (h) \in T$
18	14 15 16 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to s (h) \in T$
19	1 4 5 6 12 13	tendotr	$⊢ ((K \in HL \land W \in H) \land (s \in E \land s \neq \underset{˙}{0}) \land h \in T) \to R (s (h)) = R (h)$
20	19	3com23	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to R (s (h)) = R (h)$
21		eqid	$⊢ oc (K) = oc (K)$
22		eqid	$⊢ Atoms (K) = Atoms (K)$
23	1 2 3 21 22 4 5 6 7 8 9 10 11 12	cdlemk56w	$⊢ ((K \in HL \land W \in H) \land (s (h) \in T \land h \in T) \land R (s (h)) = R (h)) \to (U \in E \land U (s (h)) = h)$
24	14 18 16 20 23	syl121anc	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to (U \in E \land U (s (h)) = h)$

Metamath Proof Explorer

Theorem cdleml6

Proof