cdlemk11

Description: Part of proof of Lemma K of Crawley p. 118. Eq. 3, line 8, p. 119. (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.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
	cdlemk.v	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
Assertion	cdlemk11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (G) (P) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} 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.s	$⊢ S = (f \in T ⟼ (ι i \in T \| i (P) = (P \underset{˙}{\lor} R (f)) \underset{˙}{\land} (N (P) \underset{˙}{\lor} R (f \circ F^{-1}))))$
10		cdlemk.v	$⊢ V = (G (P) \underset{˙}{\lor} X (P)) \underset{˙}{\land} (R (G \circ F^{-1}) \underset{˙}{\lor} R (X \circ F^{-1}))$
11		simp11l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to K \in HL$
12	11	hllatd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to K \in Lat$
13		simp1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to ((K \in HL \land W \in H) \land F \in T \land G \in T)$
14		simp21l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to N \in T$
15		simp22	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
16		simp23	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to R (F) = R (N)$
17		simp311	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to F \neq {I ↾}_{B}$
18		simp312	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to G \neq {I ↾}_{B}$
19		simp32	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to R (G) \neq R (F)$
20	1 2 3 4 5 6 7 8 9	cdlemksat	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (G) \neq R (F))) \to S (G) (P) \in A$
21	13 14 15 16 17 18 19 20	syl133anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (G) (P) \in A$
22	1 4	atbase	$⊢ S (G) (P) \in A \to S (G) (P) \in B$
23	21 22	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (G) (P) \in B$
24		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to (K \in HL \land W \in H)$
25		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to F \in T$
26		simp21r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to X \in T$
27		simp313	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to X \neq {I ↾}_{B}$
28		simp33	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to R (X) \neq R (F)$
29	1 2 3 4 5 6 7 8 9	cdlemksat	$⊢ (((K \in HL \land W \in H) \land F \in T \land X \in T) \land (N \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land (F \neq {I ↾}_{B} \land X \neq {I ↾}_{B} \land R (X) \neq R (F))) \to S (X) (P) \in A$
30	24 25 26 14 15 16 17 27 28 29	syl333anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (X) (P) \in A$
31	1 4	atbase	$⊢ S (X) (P) \in A \to S (X) (P) \in B$
32	30 31	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (X) (P) \in B$
33		simp11r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to W \in H$
34		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to G \in T$
35		simp22l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to P \in A$
36	1 2 3 4 5 6 7 8 10	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$
37	11 33 25 34 26 35 36	syl231anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to V \in B$
38	1 3	latjcl	$⊢ (K \in Lat \land S (X) (P) \in B \land V \in B) \to S (X) (P) \underset{˙}{\lor} V \in B$
39	12 32 37 38	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (X) (P) \underset{˙}{\lor} V \in B$
40	5 6	ltrncnv	$⊢ ((K \in HL \land W \in H) \land G \in T) \to G^{-1} \in T$
41	24 34 40	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to G^{-1} \in T$
42	5 6	ltrnco	$⊢ ((K \in HL \land W \in H) \land X \in T \land G^{-1} \in T) \to X \circ G^{-1} \in T$
43	24 26 41 42	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to X \circ G^{-1} \in T$
44	1 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land X \circ G^{-1} \in T) \to R (X \circ G^{-1}) \in B$
45	24 43 44	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to R (X \circ G^{-1}) \in B$
46	1 3	latjcl	$⊢ (K \in Lat \land S (X) (P) \in B \land R (X \circ G^{-1}) \in B) \to S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}) \in B$
47	12 32 45 46	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}) \in B$
48	1 2 3 4 5 6 7 8 9 10	cdlemk7	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (G) (P) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} V)$
49	1 2 3 4 5 6 7 8 10	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})$
50	11 33 25 34 26 15 49	syl231anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to V \underset{˙}{\leq} R (X \circ G^{-1})$
51	1 2 3	latjlej2	$⊢ (K \in Lat \land (V \in B \land R (X \circ G^{-1}) \in B \land S (X) (P) \in B)) \to (V \underset{˙}{\leq} R (X \circ G^{-1}) \to (S (X) (P) \underset{˙}{\lor} V) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})))$
52	12 37 45 32 51	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to (V \underset{˙}{\leq} R (X \circ G^{-1}) \to (S (X) (P) \underset{˙}{\lor} V) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1})))$
53	50 52	mpd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to (S (X) (P) \underset{˙}{\lor} V) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$
54	1 2 12 23 39 47 48 53	lattrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((N \in T \land X \in T) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (F) = R (N)) \land ((F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land X \neq {I ↾}_{B}) \land R (G) \neq R (F) \land R (X) \neq R (F))) \to S (G) (P) \underset{˙}{\leq} (S (X) (P) \underset{˙}{\lor} R (X \circ G^{-1}))$

Metamath Proof Explorer

Theorem cdlemk11

Proof