cdlemi

	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)$
	cdlemi.s	$⊢ S = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
Assertion	cdlemi	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) = S$

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		cdlemi.s	$⊢ S = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
11		simp11l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in HL$
12		simp11r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to W \in H$
13		simp2l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U \in E$
14		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \in T$
15		simp2r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
16	1 2 3 4 5 6 7 8 9	cdlemi1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land G \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
17	11 12 13 14 15 16	syl221anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
18		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F \in T$
19	1 2 3 4 5 6 7 8 9	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}))$
20	11 12 13 18 14 15 19	syl231anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) \underset{˙}{\leq} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
21	11	hllatd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in Lat$
22		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (K \in HL \land W \in H)$
23	6 7 9	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land G \in T) \to U (G) \in T$
24	22 13 14 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) \in T$
25		simp2rl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \in A$
26	1 5	atbase	$⊢ P \in A \to P \in B$
27	25 26	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \in B$
28	1 6 7	ltrncl	$⊢ ((K \in HL \land W \in H) \land U (G) \in T \land P \in B) \to U (G) (P) \in B$
29	22 24 27 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) \in B$
30	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in B$
31	22 14 30	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \in B$
32	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land R (G) \in B) \to P \underset{˙}{\lor} R (G) \in B$
33	21 27 31 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \underset{˙}{\lor} R (G) \in B$
34	6 7 9	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land F \in T) \to U (F) \in T$
35	22 13 18 34	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (F) \in T$
36	1 6 7	ltrncl	$⊢ ((K \in HL \land W \in H) \land U (F) \in T \land P \in B) \to U (F) (P) \in B$
37	22 35 27 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (F) (P) \in B$
38	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
39	22 18 38	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F^{-1} \in T$
40	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$
41	22 14 39 40	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \circ F^{-1} \in T$
42	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T) \to R (G \circ F^{-1}) \in B$
43	22 41 42	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \in B$
44	1 3	latjcl	$⊢ (K \in Lat \land U (F) (P) \in B \land R (G \circ F^{-1}) \in B) \to U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
45	21 37 43 44	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
46	1 2 4	latlem12	$⊢ (K \in Lat \land (U (G) (P) \in B \land P \underset{˙}{\lor} R (G) \in B \land U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}) \in B)) \to ((U (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G)) \land U (G) (P) \underset{˙}{\leq} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \leftrightarrow U (G) (P) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))))$
47	21 29 33 45 46	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to ((U (G) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G)) \land U (G) (P) \underset{˙}{\leq} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \leftrightarrow U (G) (P) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))))$
48	17 20 47	mpbi2and	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})))$
49		hlatl	$⊢ K \in HL \to K \in AtLat$
50	11 49	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in AtLat$
51	2 5 6 7	ltrnat	$⊢ ((K \in HL \land W \in H) \land U (G) \in T \land P \in A) \to U (G) (P) \in A$
52	22 24 25 51	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) \in A$
53	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)$
54	22 35 15 53	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (U (F) (P) \in A \land \neg U (F) (P) \underset{˙}{\leq} W)$
55	1 2 3 4 5 6 7 8 9	cdlemi1	$⊢ ((K \in HL \land W \in H) \land (U \in E \land F \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to U (F) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))$
56	11 12 13 18 15 55	syl221anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (F) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))$
57	15 54 56	3jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land (U (F) (P) \in A \land \neg U (F) (P) \underset{˙}{\leq} W) \land U (F) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)))$
58		eqid	$⊢ (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
59	1 2 3 4 5 6 7 8 58	cdlemh	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (U (F) (P) \in A \land \neg U (F) (P) \underset{˙}{\leq} W) \land U (F) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})) \in A \land \neg ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\leq} W)$
60	59	simpld	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (U (F) (P) \in A \land \neg U (F) (P) \underset{˙}{\leq} W) \land U (F) (P) \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})) \in A$
61	57 60	syld3an2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})) \in A$
62	2 5	atcmp	$⊢ (K \in AtLat \land U (G) (P) \in A \land (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})) \in A) \to (U (G) (P) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \leftrightarrow U (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})))$
63	50 52 61 62	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (U (G) (P) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))) \leftrightarrow U (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1})))$
64	48 63	mpbid	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (U (F) (P) \underset{˙}{\lor} R (G \circ F^{-1}))$
65	64 10	eqtr4di	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (U \in E \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to U (G) (P) = S$

Metamath Proof Explorer

Theorem cdlemi

Proof