cdlemi2

Description: Part of proof of Lemma I of Crawley p. 118. (Contributed by NM, 18-Jun-2013)

	Ref	Expression
Hypotheses	cdlemi.b	$⊢ B = {Base}_{K}$
	cdlemi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemi.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemi.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemi.a	$⊢ A = Atoms (K)$
	cdlemi.h	$⊢ H = LHyp (K)$
	cdlemi.t	$⊢ T = LTrn (K) (W)$
	cdlemi.r	$⊢ R = trL (K) (W)$
	cdlemi.e	$⊢ E = TEndo (K) (W)$
Assertion	cdlemi2	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (G) (P) \underset{˙}{\leq} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$

Proof

Step	Hyp	Ref	Expression
1		cdlemi.b	$⊢ B = {Base}_{K}$
2		cdlemi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemi.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemi.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemi.a	$⊢ A = Atoms (K)$
6		cdlemi.h	$⊢ H = LHyp (K)$
7		cdlemi.t	$⊢ T = LTrn (K) (W)$
8		cdlemi.r	$⊢ R = trL (K) (W)$
9		cdlemi.e	$⊢ E = TEndo (K) (W)$
10		simp1l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in HL$
11		simp1r	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in H$
12		simp21	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U \in E$
13		simp1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
14		simp23	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \in T$
15		simp22	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F \in T$
16	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
17	13 15 16	syl2anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F^{-1} \in T$
18	6 7	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F^{-1} \in T) \to G \circ F^{-1} \in T$
19	13 14 17 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ F^{-1} \in T$
20	6 7 9	tendovalco	$⊢ ((K \in HL \land W \in H \land U \in E) \land (G \circ F^{-1} \in T \land F \in T)) \to U ((G \circ F^{-1}) \circ F) = U (G \circ F^{-1}) \circ U (F)$
21	10 11 12 19 15 20	syl32anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U ((G \circ F^{-1}) \circ F) = U (G \circ F^{-1}) \circ U (F)$
22		coass	$⊢ (G \circ F^{-1}) \circ F = G \circ (F^{-1} \circ F)$
23	1 6 7	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
24	13 15 23	syl2anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F : B \underset{1-1 onto}{⟶} B$
25		f1ococnv1	$⊢ F : B \underset{1-1 onto}{⟶} B \to F^{-1} \circ F = {I ↾}_{B}$
26	24 25	syl	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F^{-1} \circ F = {I ↾}_{B}$
27	26	coeq2d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ (F^{-1} \circ F) = G \circ ({I ↾}_{B})$
28	1 6 7	ltrn1o	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G : B \underset{1-1 onto}{⟶} B$
29	13 14 28	syl2anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G : B \underset{1-1 onto}{⟶} B$
30		f1of	$⊢ G : B \underset{1-1 onto}{⟶} B \to G : B ⟶ B$
31		fcoi1	$⊢ G : B ⟶ B \to G \circ ({I ↾}_{B}) = G$
32	29 30 31	3syl	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ ({I ↾}_{B}) = G$
33	27 32	eqtrd	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ (F^{-1} \circ F) = G$
34	22 33	eqtrid	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G \circ F^{-1}) \circ F = G$
35	34	fveq2d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U ((G \circ F^{-1}) \circ F) = U (G)$
36	21 35	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (G \circ F^{-1}) \circ U (F) = U (G)$
37	36	fveq1d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (U (G \circ F^{-1}) \circ U (F)) (P) = U (G) (P)$
38	6 7 9	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land G \circ F^{-1} \in T) \to U (G \circ F^{-1}) \in T$
39	13 12 19 38	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (G \circ F^{-1}) \in T$
40	6 7 9	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land F \in T) \to U (F) \in T$
41	13 12 15 40	syl3anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (F) \in T$
42		simp3l	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
43	2 5 6 7	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (U (G \circ F^{-1}) \in T \land U (F) \in T) \land P \in A) \to (U (G \circ F^{-1}) \circ U (F)) (P) = U (G \circ F^{-1}) (U (F) (P))$
44	13 39 41 42 43	syl121anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (U (G \circ F^{-1}) \circ U (F)) (P) = U (G \circ F^{-1}) (U (F) (P))$
45	37 44	eqtr3d	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (G) (P) = U (G \circ F^{-1}) (U (F) (P))$
46	2 5 6 7	ltrnel	$⊢ ((K \in HL \land W \in H) \land U (F) \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (U (F) (P) \in A \land \neg U (F) (P) \underset{˙}{\leq} W)$
47	41 46	syld3an2	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (U (F) (P) \in A \land \neg U (F) (P) \underset{˙}{\leq} W)$
48	1 2 3 4 5 6 7 8 9	cdlemi1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land G \circ F^{-1} \in T) \land (U (F) (P) \in A \land \neg U (F) (P) \underset{˙}{\leq} W)) \to U (G \circ F^{-1}) (U (F) (P)) \underset{˙}{\leq} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
49	13 12 19 47 48	syl121anc	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (G \circ F^{-1}) (U (F) (P)) \underset{˙}{\leq} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
50	45 49	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (G) (P) \underset{˙}{\leq} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$

Metamath Proof Explorer

Theorem cdlemi2

Proof