cdlemk10

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 29-Jun-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)$
	cdlemk.v1	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
Assertion	cdlemk10	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to V \underset{˙}{\leq} R (X \circ G^{-1})$

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		cdlemk.v1	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
10		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
11		simp22	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \in T$
12		simp21	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F \in T$
13	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
14	10 12 13	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F^{-1} \in T$
15	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$
16	10 11 14 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G \circ F^{-1} \in T$
17	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$
18	10 16 17	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (G \circ F^{-1}) \underset{˙}{\leq} W$
19		simp23	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \in T$
20	5 6	ltrnco	$⊢ ((K \in HL \land W \in H) \land X \in T \land F^{-1} \in T) \to X \circ F^{-1} \in T$
21	10 19 14 20	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X \circ F^{-1} \in T$
22	2 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land X \circ F^{-1} \in T) \to R (X \circ F^{-1}) \underset{˙}{\leq} W$
23	10 21 22	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (X \circ F^{-1}) \underset{˙}{\leq} W$
24		simp1l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in HL$
25	24	hllatd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in Lat$
26	1 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T) \to R (G \circ F^{-1}) \in B$
27	10 16 26	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (G \circ F^{-1}) \in B$
28	1 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land X \circ F^{-1} \in T) \to R (X \circ F^{-1}) \in B$
29	10 21 28	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (X \circ F^{-1}) \in B$
30		simp1r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in H$
31	1 5	lhpbase	$⊢ W \in H \to W \in B$
32	30 31	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in B$
33	1 2 3	latjle12	$⊢ (K \in Lat \land (R (G \circ F^{-1}) \in B \land R (X \circ F^{-1}) \in B \land W \in B)) \to ((R (G \circ F^{-1}) \underset{˙}{\leq} W \land R (X \circ F^{-1}) \underset{˙}{\leq} W) \leftrightarrow (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) \underset{˙}{\leq} W)$
34	25 27 29 32 33	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((R (G \circ F^{-1}) \underset{˙}{\leq} W \land R (X \circ F^{-1}) \underset{˙}{\leq} W) \leftrightarrow (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) \underset{˙}{\leq} W)$
35	18 23 34	mpbi2and	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) \underset{˙}{\leq} W$
36	1 3	latjcl	$⊢ (K \in Lat \land R (G \circ F^{-1}) \in B \land R (X \circ F^{-1}) \in B) \to R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}) \in B$
37	25 27 29 36	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}) \in B$
38		simp3l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
39	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in A) \to G (P) \in A$
40	10 11 38 39	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \in A$
41	2 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land X \in T \land P \in A) \to X (P) \in A$
42	10 19 38 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to X (P) \in A$
43	1 3 4	hlatjcl	$⊢ (K \in HL \land G (P) \in A \land X (P) \in A) \to G (P) \underset{˙}{\lor} X (P) \in B$
44	24 40 42 43	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to G (P) \underset{˙}{\lor} X (P) \in B$
45	1 2 8	latmlem2	$⊢ (K \in Lat \land (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}) \in B \land W \in B \land G (P) \underset{˙}{\lor} X (P) \in B)) \to ((R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) \underset{˙}{\leq} W \to ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\leq} ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W))$
46	25 37 32 44 45	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) \underset{˙}{\leq} W \to ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\leq} ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W))$
47	35 46	mpd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\leq} ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W)$
48		simp3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
49	1 2 3 4 5 6 7 8	cdlemk9	$⊢ ((K \in HL \land W \in H) \land (G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W = R (X \circ G^{-1})$
50	24 30 11 19 48 49	syl221anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} W = R (X \circ G^{-1})$
51	47 50	breqtrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))) \underset{˙}{\leq} R (X \circ G^{-1})$
52	9 51	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to V \underset{˙}{\leq} R (X \circ G^{-1})$

Metamath Proof Explorer

Theorem cdlemk10

Proof