cdlemk3

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 3-Jul-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	cdlemk3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (F (P) \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} R (G \circ F^{-1})) = F (P)$

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 G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \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 G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \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 G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F \in T$
12		simp32l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F \neq {I ↾}_{B}$
13	1 4 5 6 7	trlnidat	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to R (F) \in A$
14	10 11 12 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F) \in A$
15		simp2r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G \in T$
16		simp31	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G) \neq R (F)$
17	4 5 6 7	trlcocnvat	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F \in T) \land R (G) \neq R (F)) \to R (G \circ F^{-1}) \in A$
18	10 15 11 16 17	syl121anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G \circ F^{-1}) \in A$
19		simp33l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to P \in A$
20	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$
21	10 11 19 20	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F (P) \in A$
22	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
23	10 11 22	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F^{-1} \in T$
24	5 6 7	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
25	10 11 24	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F^{-1}) = R (F)$
26	16	necomd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F) \neq R (G)$
27	25 26	eqnetrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F^{-1}) \neq R (G)$
28		simp32r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G \neq {I ↾}_{B}$
29	1 5 6 7	trlcone	$⊢ ((K \in HL \land W \in H) \land (F^{-1} \in T \land G \in T) \land (R (F^{-1}) \neq R (G) \land G \neq {I ↾}_{B})) \to R (F^{-1}) \neq R (F^{-1} \circ G)$
30	10 23 15 27 28 29	syl122anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F^{-1}) \neq R (F^{-1} \circ G)$
31	5 6	ltrncom	$⊢ ((K \in HL \land W \in H) \land F^{-1} \in T \land G \in T) \to F^{-1} \circ G = G \circ F^{-1}$
32	10 23 15 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F^{-1} \circ G = G \circ F^{-1}$
33	32	fveq2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F^{-1} \circ G) = R (G \circ F^{-1})$
34	30 25 33	3netr3d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F) \neq R (G \circ F^{-1})$
35		simp33	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
36	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)$
37	36	simprd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg F (P) \underset{˙}{\leq} W$
38	10 11 35 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to \neg F (P) \underset{˙}{\leq} W$
39	2 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
40	10 11 39	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F) \underset{˙}{\leq} W$
41	5 6	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F^{-1} \in T) \to G \circ F^{-1} \in T$
42	10 15 23 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to G \circ F^{-1} \in T$
43	2 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T) \to R (G \circ F^{-1}) \underset{˙}{\leq} W$
44	10 42 43	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G \circ F^{-1}) \underset{˙}{\leq} W$
45	9	hllatd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to K \in Lat$
46	1 4	atbase	$⊢ R (F) \in A \to R (F) \in B$
47	14 46	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F) \in B$
48	1 4	atbase	$⊢ R (G \circ F^{-1}) \in A \to R (G \circ F^{-1}) \in B$
49	18 48	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (G \circ F^{-1}) \in B$
50		simp1r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to W \in H$
51	1 5	lhpbase	$⊢ W \in H \to W \in B$
52	50 51	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to W \in B$
53	1 2 3	latjle12	$⊢ (K \in Lat \land (R (F) \in B \land R (G \circ F^{-1}) \in B \land W \in B)) \to ((R (F) \underset{˙}{\leq} W \land R (G \circ F^{-1}) \underset{˙}{\leq} W) \leftrightarrow (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} W)$
54	45 47 49 52 53	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to ((R (F) \underset{˙}{\leq} W \land R (G \circ F^{-1}) \underset{˙}{\leq} W) \leftrightarrow (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} W)$
55	40 44 54	mpbi2and	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} W$
56	1 4	atbase	$⊢ F (P) \in A \to F (P) \in B$
57	21 56	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to F (P) \in B$
58	1 3 4	hlatjcl	$⊢ (K \in HL \land R (F) \in A \land R (G \circ F^{-1}) \in A) \to R (F) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
59	9 14 18 58	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to R (F) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
60	1 2	lattr	$⊢ (K \in Lat \land (F (P) \in B \land R (F) \underset{˙}{\lor} R (G \circ F^{-1}) \in B \land W \in B)) \to ((F (P) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \land (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} W) \to F (P) \underset{˙}{\leq} W)$
61	45 57 59 52 60	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to ((F (P) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \land (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} W) \to F (P) \underset{˙}{\leq} W)$
62	55 61	mpan2d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (F (P) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G \circ F^{-1})) \to F (P) \underset{˙}{\leq} W)$
63	38 62	mtod	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to \neg F (P) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G \circ F^{-1}))$
64	2 3 8 4	2llnma2	$⊢ (K \in HL \land (R (F) \in A \land R (G \circ F^{-1}) \in A \land F (P) \in A) \land (R (F) \neq R (G \circ F^{-1}) \land \neg F (P) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} R (G \circ F^{-1})))) \to (F (P) \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} R (G \circ F^{-1})) = F (P)$
65	9 14 18 21 34 63 64	syl132anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (R (G) \neq R (F) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W))) \to (F (P) \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} R (G \circ F^{-1})) = F (P)$

Metamath Proof Explorer

Theorem cdlemk3

Proof