cdlemkvcl

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 27-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	cdlemkvcl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to V \in B$

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		simp1l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to K \in HL$
11	10	hllatd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to K \in Lat$
12		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to (K \in HL \land W \in H)$
13		simp22	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to G \in T$
14	1 4	atbase	$⊢ P \in A \to P \in B$
15	14	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to P \in B$
16	1 5 6	ltrncl	$⊢ ((K \in HL \land W \in H) \land G \in T \land P \in B) \to G (P) \in B$
17	12 13 15 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to G (P) \in B$
18		simp23	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to X \in T$
19	1 5 6	ltrncl	$⊢ ((K \in HL \land W \in H) \land X \in T \land P \in B) \to X (P) \in B$
20	12 18 15 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to X (P) \in B$
21	1 3	latjcl	$⊢ (K \in Lat \land G (P) \in B \land X (P) \in B) \to G (P) \underset{˙}{\lor} X (P) \in B$
22	11 17 20 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to G (P) \underset{˙}{\lor} X (P) \in B$
23		simp21	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to F \in T$
24	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
25	12 23 24	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to F^{-1} \in T$
26	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$
27	12 13 25 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to G \circ F^{-1} \in T$
28	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$
29	12 27 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) \to R (G \circ F^{-1}) \in B$
30	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$
31	12 18 25 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to X \circ F^{-1} \in T$
32	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$
33	12 31 32	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to R (X \circ F^{-1}) \in B$
34	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$
35	11 29 33 34	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}) \in B$
36	1 8	latmcl	$⊢ (K \in Lat \land G (P) \underset{˙}{\lor} X (P) \in B \land R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}) \in B) \to (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) \in B$
37	11 22 35 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) \to (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1})) \in B$
38	9 37	eqeltrid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T \land X \in T) \land P \in A) \to V \in B$

Metamath Proof Explorer

Theorem cdlemkvcl

Proof