cdlemkid1

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

Proof

Step	Hyp	Ref	Expression
1		cdlemk5.b	$⊢ B = {Base}_{K}$
2		cdlemk5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemk5.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemk5.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemk5.a	$⊢ A = Atoms (K)$
6		cdlemk5.h	$⊢ H = LHyp (K)$
7		cdlemk5.t	$⊢ T = LTrn (K) (W)$
8		cdlemk5.r	$⊢ R = trL (K) (W)$
9		cdlemk5.z	$⊢ Z = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))$
10	9	oveq1i	$⊢ Z \underset{˙}{\lor} R (b) = ((P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))) \underset{˙}{\lor} R (b)$
11		simp1l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to K \in HL$
12		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (K \in HL \land W \in H)$
13		simp3rl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to b \in T$
14		simp3rr	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to b \neq {I ↾}_{B}$
15	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$
16	12 13 14 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b) \in A$
17		simp3ll	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to P \in A$
18	1 3 5	hlatjcl	$⊢ (K \in HL \land P \in A \land R (b) \in A) \to P \underset{˙}{\lor} R (b) \in B$
19	11 17 16 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to P \underset{˙}{\lor} R (b) \in B$
20	11	hllatd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to K \in Lat$
21		simp22	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to N \in T$
22	1 5	atbase	$⊢ P \in A \to P \in B$
23	17 22	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to P \in B$
24	1 6 7	ltrncl	$⊢ ((K \in HL \land W \in H) \land N \in T \land P \in B) \to N (P) \in B$
25	12 21 23 24	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to N (P) \in B$
26		simp21	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to F \in T$
27	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
28	12 26 27	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to F^{-1} \in T$
29	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$
30	12 13 28 29	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to b \circ F^{-1} \in T$
31	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$
32	12 30 31	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b \circ F^{-1}) \in B$
33	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$
34	20 25 32 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to N (P) \underset{˙}{\lor} R (b \circ F^{-1}) \in B$
35	2 3 5	hlatlej2	$⊢ (K \in HL \land P \in A \land R (b) \in A) \to R (b) \underset{˙}{\leq} (P \underset{˙}{\lor} R (b))$
36	11 17 16 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b) \underset{˙}{\leq} (P \underset{˙}{\lor} R (b))$
37	1 2 3 4 5	atmod2i1	$⊢ (K \in HL \land (R (b) \in A \land P \underset{˙}{\lor} R (b) \in B \land N (P) \underset{˙}{\lor} R (b \circ F^{-1}) \in B) \land R (b) \underset{˙}{\leq} (P \underset{˙}{\lor} R (b))) \to ((P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))) \underset{˙}{\lor} R (b) = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} ((N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \underset{˙}{\lor} R (b))$
38	11 16 19 34 36 37	syl131anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to ((P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))) \underset{˙}{\lor} R (b) = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} ((N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \underset{˙}{\lor} R (b))$
39	1 5	atbase	$⊢ R (b) \in A \to R (b) \in B$
40	16 39	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b) \in B$
41	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land N \in T) \to R (N) \in B$
42	12 21 41	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (N) \in B$
43	1 3	latj32	$⊢ (K \in Lat \land (P \in B \land R (b) \in B \land R (N) \in B)) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\lor} R (N) = (P \underset{˙}{\lor} R (N)) \underset{˙}{\lor} R (b)$
44	20 23 40 42 43	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\lor} R (N) = (P \underset{˙}{\lor} R (N)) \underset{˙}{\lor} R (b)$
45		simp3l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
46	2 3 5 6 7 8	trljat3	$⊢ ((K \in HL \land W \in H) \land N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (N) = N (P) \underset{˙}{\lor} R (N)$
47	12 21 45 46	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to P \underset{˙}{\lor} R (N) = N (P) \underset{˙}{\lor} R (N)$
48	47	oveq1d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R (N)) \underset{˙}{\lor} R (b) = (N (P) \underset{˙}{\lor} R (N)) \underset{˙}{\lor} R (b)$
49	1 3	latjass	$⊢ (K \in Lat \land (N (P) \in B \land R (N) \in B \land R (b) \in B)) \to (N (P) \underset{˙}{\lor} R (N)) \underset{˙}{\lor} R (b) = N (P) \underset{˙}{\lor} (R (N) \underset{˙}{\lor} R (b))$
50	20 25 42 40 49	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (N (P) \underset{˙}{\lor} R (N)) \underset{˙}{\lor} R (b) = N (P) \underset{˙}{\lor} (R (N) \underset{˙}{\lor} R (b))$
51	44 48 50	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\lor} R (N) = N (P) \underset{˙}{\lor} (R (N) \underset{˙}{\lor} R (b))$
52	1 3	latjass	$⊢ (K \in Lat \land (N (P) \in B \land R (b \circ F^{-1}) \in B \land R (b) \in B)) \to (N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \underset{˙}{\lor} R (b) = N (P) \underset{˙}{\lor} (R (b \circ F^{-1}) \underset{˙}{\lor} R (b))$
53	20 25 32 40 52	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \underset{˙}{\lor} R (b) = N (P) \underset{˙}{\lor} (R (b \circ F^{-1}) \underset{˙}{\lor} R (b))$
54	1 3	latjcom	$⊢ (K \in Lat \land R (N) \in B \land R (b) \in B) \to R (N) \underset{˙}{\lor} R (b) = R (b) \underset{˙}{\lor} R (N)$
55	20 42 40 54	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (N) \underset{˙}{\lor} R (b) = R (b) \underset{˙}{\lor} R (N)$
56	6 7 8	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
57	12 26 56	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (F^{-1}) = R (F)$
58		simp23	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (F) = R (N)$
59	57 58	eqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (F^{-1}) = R (N)$
60	59	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b) \underset{˙}{\lor} R (F^{-1}) = R (b) \underset{˙}{\lor} R (N)$
61	55 60	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (N) \underset{˙}{\lor} R (b) = R (b) \underset{˙}{\lor} R (F^{-1})$
62	3 6 7 8	trljco	$⊢ ((K \in HL \land W \in H) \land b \in T \land F^{-1} \in T) \to R (b) \underset{˙}{\lor} R (b \circ F^{-1}) = R (b) \underset{˙}{\lor} R (F^{-1})$
63	12 13 28 62	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b) \underset{˙}{\lor} R (b \circ F^{-1}) = R (b) \underset{˙}{\lor} R (F^{-1})$
64	1 3	latjcom	$⊢ (K \in Lat \land R (b) \in B \land R (b \circ F^{-1}) \in B) \to R (b) \underset{˙}{\lor} R (b \circ F^{-1}) = R (b \circ F^{-1}) \underset{˙}{\lor} R (b)$
65	20 40 32 64	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b) \underset{˙}{\lor} R (b \circ F^{-1}) = R (b \circ F^{-1}) \underset{˙}{\lor} R (b)$
66	61 63 65	3eqtr2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to R (N) \underset{˙}{\lor} R (b) = R (b \circ F^{-1}) \underset{˙}{\lor} R (b)$
67	66	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to N (P) \underset{˙}{\lor} (R (N) \underset{˙}{\lor} R (b)) = N (P) \underset{˙}{\lor} (R (b \circ F^{-1}) \underset{˙}{\lor} R (b))$
68	53 67	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \underset{˙}{\lor} R (b) = N (P) \underset{˙}{\lor} (R (N) \underset{˙}{\lor} R (b))$
69	51 68	eqtr4d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\lor} R (N) = (N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \underset{˙}{\lor} R (b)$
70	69	oveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} ((P \underset{˙}{\lor} R (b)) \underset{˙}{\lor} R (N)) = (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} ((N (P) \underset{˙}{\lor} R (b \circ F^{-1})) \underset{˙}{\lor} R (b))$
71	1 3 4	latabs2	$⊢ (K \in Lat \land P \underset{˙}{\lor} R (b) \in B \land R (N) \in B) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} ((P \underset{˙}{\lor} R (b)) \underset{˙}{\lor} R (N)) = P \underset{˙}{\lor} R (b)$
72	20 19 42 71	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R (b)) \underset{˙}{\land} ((P \underset{˙}{\lor} R (b)) \underset{˙}{\lor} R (N)) = P \underset{˙}{\lor} R (b)$
73	38 70 72	3eqtr2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to ((P \underset{˙}{\lor} R (b)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (b \circ F^{-1}))) \underset{˙}{\lor} R (b) = P \underset{˙}{\lor} R (b)$
74	10 73	eqtrid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land N \in T \land R (F) = R (N)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))) \to Z \underset{˙}{\lor} R (b) = P \underset{˙}{\lor} R (b)$

Metamath Proof Explorer

Theorem cdlemkid1

Proof