cdlemk37

Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk4.b	$⊢ B = {Base}_{K}$
	cdlemk4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemk4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemk4.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemk4.a	$⊢ A = Atoms (K)$
	cdlemk4.h	$⊢ H = LHyp (K)$
	cdlemk4.t	$⊢ T = LTrn (K) (W)$
	cdlemk4.r	$⊢ R = trL (K) (W)$
	cdlemk4.z	$⊢ Z = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))$
	cdlemk4.y	$⊢ Y = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (G \circ b^{-1}))$
	cdlemk4.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = Y))$
Assertion	cdlemk37	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to X (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$

Proof

Step	Hyp	Ref	Expression
1		cdlemk4.b	$⊢ B = {Base}_{K}$
2		cdlemk4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk4.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk4.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemk4.a	$⊢ A = Atoms (K)$
6		cdlemk4.h	$⊢ H = LHyp (K)$
7		cdlemk4.t	$⊢ T = LTrn (K) (W)$
8		cdlemk4.r	$⊢ R = trL (K) (W)$
9		cdlemk4.z	$⊢ Z = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))$
10		cdlemk4.y	$⊢ Y = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (G \circ b^{-1}))$
11		cdlemk4.x	$⊢ X = (ι z \in T \| \forall b \in T ((b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)) \to z (P) = Y))$
12	1 2 3 4 5 6 7 8 9 10 11	cdlemk36	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to X (P) = Y$
13		simp11l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to K \in HL$
14	13	hllatd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to K \in Lat$
15		simp22l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to P \in A$
16		simp11	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to (K \in HL \land W \in H)$
17		simp13l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to G \in T$
18		simp13r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to G \neq {I ↾}_{B}$
19	1 5 6 7 8	trlnidat	$⊢ ((K \in HL \land W \in H) \land G \in T \land G \neq {I ↾}_{B}) \to R (G) \in A$
20	16 17 18 19	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to R (G) \in A$
21	1 3 5	hlatjcl	$⊢ (K \in HL \land P \in A \land R (G) \in A) \to P \underset{˙}{\lor} R (G) \in B$
22	13 15 20 21	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to P \underset{˙}{\lor} R (G) \in B$
23		simp3l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to b \in T$
24		simp3r1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to b \neq {I ↾}_{B}$
25	1 5 6 7 8	trlnidat	$⊢ ((K \in HL \land W \in H) \land b \in T \land b \neq {I ↾}_{B}) \to R (b) \in A$
26	16 23 24 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to R (b) \in A$
27	1 3 5	hlatjcl	$⊢ (K \in HL \land P \in A \land R (b) \in A) \to P \underset{˙}{\lor} R (b) \in B$
28	13 15 26 27	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to P \underset{˙}{\lor} R (b) \in B$
29		simp21	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to N \in T$
30	2 5 6 7	ltrnat	$⊢ ((K \in HL \land W \in H) \land N \in T \land P \in A) \to N (P) \in A$
31	16 29 15 30	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to N (P) \in A$
32	1 5	atbase	$⊢ N (P) \in A \to N (P) \in B$
33	31 32	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to N (P) \in B$
34		simp12l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to F \in T$
35	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
36	16 34 35	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to F^{-1} \in T$
37	6 7	ltrnco	$⊢ ((K \in HL \land W \in H) \land b \in T \land F^{-1} \in T) \to b \circ F^{-1} \in T$
38	16 23 36 37	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to b \circ F^{-1} \in T$
39	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land b \circ F^{-1} \in T) \to R (b \circ F^{-1}) \in B$
40	16 38 39	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to R (b \circ F^{-1}) \in B$
41	1 3	latjcl	$⊢ (K \in Lat \land N (P) \in B \land R (b \circ F^{-1}) \in B) \to N (P) \underset{˙}{\lor} R (b \circ F^{-1}) \in B$
42	14 33 40 41	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to N (P) \underset{˙}{\lor} R (b \circ F^{-1}) \in B$
43	1 4	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} R (b) \in B \land N (P) \underset{˙}{\lor} R (b \circ F^{-1}) \in B) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \in B$
44	14 28 42 43	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \in B$
45	9 44	eqeltrid	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to Z \in B$
46	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land b \in T) \to b^{-1} \in T$
47	16 23 46	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to b^{-1} \in T$
48	6 7	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land b^{-1} \in T) \to G \circ b^{-1} \in T$
49	16 17 47 48	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to G \circ b^{-1} \in T$
50	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land G \circ b^{-1} \in T) \to R (G \circ b^{-1}) \in B$
51	16 49 50	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to R (G \circ b^{-1}) \in B$
52	1 3	latjcl	$⊢ (K \in Lat \land Z \in B \land R (G \circ b^{-1}) \in B) \to Z \underset{˙}{\lor} R (G \circ b^{-1}) \in B$
53	14 45 51 52	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to Z \underset{˙}{\lor} R (G \circ b^{-1}) \in B$
54	1 2 4	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} R (G) \in B \land Z \underset{˙}{\lor} R (G \circ b^{-1}) \in B) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (G \circ b^{-1}))) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
55	14 22 53 54	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (G \circ b^{-1}))) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
56	10 55	eqbrtrid	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to Y \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
57	12 56	eqbrtrd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (G \in T \land G \neq {I ↾}_{B})) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (b \in T \land (b \neq {I ↾}_{B} \land R (b) \neq R (F) \land R (b) \neq R (G)))) \to X (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$

Metamath Proof Explorer

Theorem cdlemk37

Proof