cdlemk4

Description: Part of proof of Lemma K of Crawley p. 118, last line. We use X for their h, since H is already used. (Contributed by NM, 24-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	$⊢ B = {Base}_{K}$
2		cdlemk.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk.a	$⊢ A = Atoms (K)$
5		cdlemk.h	$⊢ H = LHyp (K)$
6		cdlemk.t	$⊢ T = LTrn (K) (W)$
7		cdlemk.r	$⊢ R = trL (K) (W)$
8		cdlemk.m	$⊢ \underset{˙}{\land} = meet (K)$
9		simp1l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in HL$
10		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
11		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F \in T$
12		simp3l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
13	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
14	10 11 12 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \in A$
15		simp2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \in T$
16	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land X \in T \land P \in A) \to X (P) \in A$
17	10 15 12 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) \in A$
18	2 3 4	hlatlej1	$⊢ (K \in HL \land F (P) \in A \land X (P) \in A) \to F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} X (P))$
19	9 14 17 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} X (P))$
20	9	hllatd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in Lat$
21	1 4	atbase	$⊢ F (P) \in A \to F (P) \in B$
22	14 21	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \in B$
23	1 4	atbase	$⊢ X (P) \in A \to X (P) \in B$
24	17 23	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) \in B$
25	1 3	latjcl	$⊢ (K \in Lat \land F (P) \in B \land X (P) \in B) \to F (P) \underset{˙}{\lor} X (P) \in B$
26	20 22 24 25	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} X (P) \in B$
27		simp1r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in H$
28	1 5	lhpbase	$⊢ W \in H \to W \in B$
29	27 28	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in B$
30	2 3 4	hlatlej2	$⊢ (K \in HL \land F (P) \in A \land X (P) \in A) \to X (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} X (P))$
31	9 14 17 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} X (P))$
32	1 2 3 8 4	atmod3i1	$⊢ (K \in HL \land (X (P) \in A \land F (P) \underset{˙}{\lor} X (P) \in B \land W \in B) \land X (P) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} X (P))) \to X (P) \underset{˙}{\lor} ((F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W) = (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (X (P) \underset{˙}{\lor} W)$
33	9 17 26 29 31 32	syl131anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) \underset{˙}{\lor} ((F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W) = (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (X (P) \underset{˙}{\lor} W)$
34	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
35	10 11 34	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F^{-1} \in T$
36	5 6	ltrnco	$⊢ ((K \in HL \land W \in H) \land X \in T \land F^{-1} \in T) \to X \circ F^{-1} \in T$
37	10 15 35 36	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ F^{-1} \in T$
38	2 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
39	11 38	syld3an2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
40	2 3 8 4 5 6 7	trlval2	$⊢ ((K \in HL \land W \in H) \land X \circ F^{-1} \in T \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to R (X \circ F^{-1}) = (F (P) \underset{˙}{\lor} (X \circ F^{-1}) (F (P))) \underset{˙}{\land} W$
41	10 37 39 40	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (X \circ F^{-1}) = (F (P) \underset{˙}{\lor} (X \circ F^{-1}) (F (P))) \underset{˙}{\land} W$
42	1 5 6	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
43	10 11 42	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F : B \underset{1-1 onto}{⟶} B$
44		f1ococnv1	$⊢ F : B \underset{1-1 onto}{⟶} B \to F^{-1} \circ F = {I ↾}_{B}$
45	43 44	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F^{-1} \circ F = {I ↾}_{B}$
46	45	coeq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ (F^{-1} \circ F) = X \circ ({I ↾}_{B})$
47	1 5 6	ltrn1o	$⊢ ((K \in HL \land W \in H) \land X \in T) \to X : B \underset{1-1 onto}{⟶} B$
48	10 15 47	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X : B \underset{1-1 onto}{⟶} B$
49		f1of	$⊢ X : B \underset{1-1 onto}{⟶} B \to X : B ⟶ B$
50		fcoi1	$⊢ X : B ⟶ B \to X \circ ({I ↾}_{B}) = X$
51	48 49 50	3syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ ({I ↾}_{B}) = X$
52	46 51	eqtr2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X = X \circ (F^{-1} \circ F)$
53		coass	$⊢ (X \circ F^{-1}) \circ F = X \circ (F^{-1} \circ F)$
54	52 53	eqtr4di	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X = (X \circ F^{-1}) \circ F$
55	54	fveq1d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) = ((X \circ F^{-1}) \circ F) (P)$
56	2 4 5 6	ltrncoval	$⊢ ((K \in HL \land W \in H) \land (X \circ F^{-1} \in T \land F \in T) \land P \in A) \to ((X \circ F^{-1}) \circ F) (P) = (X \circ F^{-1}) (F (P))$
57	10 37 11 12 56	syl121anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((X \circ F^{-1}) \circ F) (P) = (X \circ F^{-1}) (F (P))$
58	55 57	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) = (X \circ F^{-1}) (F (P))$
59	58	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} X (P) = F (P) \underset{˙}{\lor} (X \circ F^{-1}) (F (P))$
60	59	eqcomd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} (X \circ F^{-1}) (F (P)) = F (P) \underset{˙}{\lor} X (P)$
61	60	oveq1d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} (X \circ F^{-1}) (F (P))) \underset{˙}{\land} W = (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W$
62	41 61	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (X \circ F^{-1}) = (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W$
63	62	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) \underset{˙}{\lor} R (X \circ F^{-1}) = X (P) \underset{˙}{\lor} ((F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W)$
64	2 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land X \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (X (P) \in A \land \neg X (P) \underset{˙}{\leq} W)$
65	15 64	syld3an2	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (X (P) \in A \land \neg X (P) \underset{˙}{\leq} W)$
66		eqid	$⊢ 1. (K) = 1. (K)$
67	2 3 66 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (X (P) \in A \land \neg X (P) \underset{˙}{\leq} W)) \to X (P) \underset{˙}{\lor} W = 1. (K)$
68	10 65 67	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) \underset{˙}{\lor} W = 1. (K)$
69	68	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (X (P) \underset{˙}{\lor} W) = (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} 1. (K)$
70		hlol	$⊢ K \in HL \to K \in OL$
71	9 70	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in OL$
72	1 8 66	olm11	$⊢ (K \in OL \land F (P) \underset{˙}{\lor} X (P) \in B) \to (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} 1. (K) = F (P) \underset{˙}{\lor} X (P)$
73	71 26 72	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} 1. (K) = F (P) \underset{˙}{\lor} X (P)$
74	69 73	eqtr2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} X (P) = (F (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (X (P) \underset{˙}{\lor} W)$
75	33 63 74	3eqtr4rd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\lor} X (P) = X (P) \underset{˙}{\lor} R (X \circ F^{-1})$
76	19 75	breqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \underset{˙}{\leq} (X (P) \underset{˙}{\lor} R (X \circ F^{-1}))$

Metamath Proof Explorer

Theorem cdlemk4

Proof