cdleml7

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	cdleml7	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to (U \circ s) (h) = ({I ↾}_{T}) (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	1 2 3 4 5 6 7 8 9 10 11 12 13	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)$
15	14	simprd	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to U (s (h)) = h$
16		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)$
17	14	simpld	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to U \in E$
18		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$
19		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$
20	4 5 12	tendocoval	$⊢ ((K \in HL \land W \in H) \land (U \in E \land s \in E) \land h \in T) \to (U \circ s) (h) = U (s (h))$
21	16 17 18 19 20	syl121anc	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to (U \circ s) (h) = U (s (h))$
22		fvresi	$⊢ h \in T \to ({I ↾}_{T}) (h) = h$
23	22	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to ({I ↾}_{T}) (h) = h$
24	15 21 23	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land h \in T \land (s \in E \land s \neq \underset{˙}{0})) \to (U \circ s) (h) = ({I ↾}_{T}) (h)$

Metamath Proof Explorer

Theorem cdleml7

Proof