cdlemkid2

	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}))$
	cdlemk5.y	$⊢ Y = (P \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
Assertion	cdlemkid2	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ⦋ G / g ⦌ Y = P$

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		cdlemk5.y	$⊢ Y = (P \underset{˙}{\lor} R (g)) \underset{˙}{\land} (Z \underset{˙}{\lor} R (g \circ b^{-1}))$
11		simp32	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to G = {I ↾}_{B}$
12	11	csbeq1d	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ⦋ G / g ⦌ Y = ⦋ ({I ↾}_{B}) / g ⦌ Y$
13	1 6 7	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in T$
14	13	3ad2ant1	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to {I ↾}_{B} \in T$
15	10	cdlemk41	$⊢ {I ↾}_{B} \in T \to ⦋ ({I ↾}_{B}) / g ⦌ Y = (P \underset{˙}{\lor} R ({I ↾}_{B})) \underset{˙}{\land} (Z \underset{˙}{\lor} R (({I ↾}_{B}) \circ b^{-1}))$
16	14 15	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ⦋ ({I ↾}_{B}) / g ⦌ Y = (P \underset{˙}{\lor} R ({I ↾}_{B})) \underset{˙}{\land} (Z \underset{˙}{\lor} R (({I ↾}_{B}) \circ b^{-1}))$
17		eqid	$⊢ 0. (K) = 0. (K)$
18	1 17 6 8	trlid0	$⊢ (K \in HL \land W \in H) \to R ({I ↾}_{B}) = 0. (K)$
19	18	3ad2ant1	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to R ({I ↾}_{B}) = 0. (K)$
20	19	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to P \underset{˙}{\lor} R ({I ↾}_{B}) = P \underset{˙}{\lor} 0. (K)$
21		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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to K \in HL$
22		hlol	$⊢ K \in HL \to K \in OL$
23	21 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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to K \in OL$
24		simp31l	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to P \in A$
25	1 5	atbase	$⊢ P \in A \to P \in B$
26	24 25	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to P \in B$
27	1 3 17	olj01	$⊢ (K \in OL \land P \in B) \to P \underset{˙}{\lor} 0. (K) = P$
28	23 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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to P \underset{˙}{\lor} 0. (K) = P$
29	20 28	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to P \underset{˙}{\lor} R ({I ↾}_{B}) = P$
30		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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to (K \in HL \land W \in H)$
31		simp33l	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to b \in T$
32	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land b \in T) \to b^{-1} \in T$
33	30 31 32	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to b^{-1} \in T$
34	1 6 7	ltrn1o	$⊢ ((K \in HL \land W \in H) \land b^{-1} \in T) \to b^{-1} : B \underset{1-1 onto}{⟶} B$
35	30 33 34	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to b^{-1} : B \underset{1-1 onto}{⟶} B$
36		f1of	$⊢ b^{-1} : B \underset{1-1 onto}{⟶} B \to b^{-1} : B ⟶ B$
37		fcoi2	$⊢ b^{-1} : B ⟶ B \to ({I ↾}_{B}) \circ b^{-1} = b^{-1}$
38	35 36 37	3syl	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ({I ↾}_{B}) \circ b^{-1} = b^{-1}$
39	38	fveq2d	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to R (({I ↾}_{B}) \circ b^{-1}) = R (b^{-1})$
40	6 7 8	trlcnv	$⊢ ((K \in HL \land W \in H) \land b \in T) \to R (b^{-1}) = R (b)$
41	30 31 40	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b^{-1}) = R (b)$
42	39 41	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to R (({I ↾}_{B}) \circ b^{-1}) = R (b)$
43	42	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to Z \underset{˙}{\lor} R (({I ↾}_{B}) \circ b^{-1}) = Z \underset{˙}{\lor} R (b)$
44		simp31	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
45		simp33	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to (b \in T \land b \neq {I ↾}_{B})$
46	44 45	jca	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ((P \in A \land \neg P \underset{˙}{\leq} W) \land (b \in T \land b \neq {I ↾}_{B}))$
47	1 2 3 4 5 6 7 8 9	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)$
48	46 47	syld3an3	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to Z \underset{˙}{\lor} R (b) = P \underset{˙}{\lor} R (b)$
49	43 48	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to Z \underset{˙}{\lor} R (({I ↾}_{B}) \circ b^{-1}) = P \underset{˙}{\lor} R (b)$
50	29 49	oveq12d	$⊢ ((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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R ({I ↾}_{B})) \underset{˙}{\land} (Z \underset{˙}{\lor} R (({I ↾}_{B}) \circ b^{-1})) = P \underset{˙}{\land} (P \underset{˙}{\lor} R (b))$
51	21	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to K \in Lat$
52	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land b \in T) \to R (b) \in B$
53	30 31 52	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to R (b) \in B$
54	1 3 4	latabs2	$⊢ (K \in Lat \land P \in B \land R (b) \in B) \to P \underset{˙}{\land} (P \underset{˙}{\lor} R (b)) = P$
55	51 26 53 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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to P \underset{˙}{\land} (P \underset{˙}{\lor} R (b)) = P$
56	50 55	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to (P \underset{˙}{\lor} R ({I ↾}_{B})) \underset{˙}{\land} (Z \underset{˙}{\lor} R (({I ↾}_{B}) \circ b^{-1})) = P$
57	16 56	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ⦋ ({I ↾}_{B}) / g ⦌ Y = P$
58	12 57	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 G = {I ↾}_{B} \land (b \in T \land b \neq {I ↾}_{B}))) \to ⦋ G / g ⦌ Y = P$

Metamath Proof Explorer

Theorem cdlemkid2

Proof