cdlemh1

Description: Part of proof of Lemma H of Crawley p. 118. (Contributed by NM, 17-Jun-2013)

	Ref	Expression
Hypotheses	cdlemh.b	$⊢ B = {Base}_{K}$
	cdlemh.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemh.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemh.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemh.a	$⊢ A = Atoms (K)$
	cdlemh.h	$⊢ H = LHyp (K)$
	cdlemh.t	$⊢ T = LTrn (K) (W)$
	cdlemh.r	$⊢ R = trL (K) (W)$
	cdlemh.s	$⊢ S = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
Assertion	cdlemh1	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to S \underset{˙}{\lor} R (G \circ F^{-1}) = Q \underset{˙}{\lor} R (G \circ F^{-1})$

Proof

Step	Hyp	Ref	Expression
1		cdlemh.b	$⊢ B = {Base}_{K}$
2		cdlemh.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemh.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemh.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdlemh.a	$⊢ A = Atoms (K)$
6		cdlemh.h	$⊢ H = LHyp (K)$
7		cdlemh.t	$⊢ T = LTrn (K) (W)$
8		cdlemh.r	$⊢ R = trL (K) (W)$
9		cdlemh.s	$⊢ S = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
10	9	oveq1i	$⊢ S \underset{˙}{\lor} R (G \circ F^{-1}) = ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\lor} R (G \circ F^{-1})$
11		simp11l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to K \in HL$
12		simp11	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to (K \in HL \land W \in H)$
13		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to G \in T$
14		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to F \in T$
15		simp3r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (F) \neq R (G)$
16	15	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (G) \neq R (F)$
17	5 6 7 8	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	12 13 14 16 17	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \in A$
19	11	hllatd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to K \in Lat$
20		simp2l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to P \in A$
21	1 5	atbase	$⊢ P \in A \to P \in B$
22	20 21	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to P \in B$
23	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in B$
24	12 13 23	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (G) \in B$
25	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land R (G) \in B) \to P \underset{˙}{\lor} R (G) \in B$
26	19 22 24 25	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to P \underset{˙}{\lor} R (G) \in B$
27		simp2r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to Q \in A$
28	1 3 5	hlatjcl	$⊢ (K \in HL \land Q \in A \land R (G \circ F^{-1}) \in A) \to Q \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
29	11 27 18 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to Q \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
30	2 3 5	hlatlej2	$⊢ (K \in HL \land Q \in A \land R (G \circ F^{-1}) \in A) \to R (G \circ F^{-1}) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
31	11 27 18 30	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
32	1 2 3 4 5	atmod4i1	$⊢ (K \in HL \land (R (G \circ F^{-1}) \in A \land P \underset{˙}{\lor} R (G) \in B \land Q \underset{˙}{\lor} R (G \circ F^{-1}) \in B) \land R (G \circ F^{-1}) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\lor} R (G \circ F^{-1}) = ((P \underset{˙}{\lor} R (G)) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
33	11 18 26 29 31 32	syl131anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\lor} R (G \circ F^{-1}) = ((P \underset{˙}{\lor} R (G)) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
34	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
35	12 14 34	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to F^{-1} \in T$
36	3 6 7 8	trljco2	$⊢ ((K \in HL \land W \in H) \land G \in T \land F^{-1} \in T) \to R (G) \underset{˙}{\lor} R (G \circ F^{-1}) = R (F^{-1}) \underset{˙}{\lor} R (G \circ F^{-1})$
37	12 13 35 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (G) \underset{˙}{\lor} R (G \circ F^{-1}) = R (F^{-1}) \underset{˙}{\lor} R (G \circ F^{-1})$
38	6 7 8	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
39	12 14 38	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (F^{-1}) = R (F)$
40	39	oveq1d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (F^{-1}) \underset{˙}{\lor} R (G \circ F^{-1}) = R (F) \underset{˙}{\lor} R (G \circ F^{-1})$
41	37 40	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (G) \underset{˙}{\lor} R (G \circ F^{-1}) = R (F) \underset{˙}{\lor} R (G \circ F^{-1})$
42	41	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to P \underset{˙}{\lor} (R (G) \underset{˙}{\lor} R (G \circ F^{-1})) = P \underset{˙}{\lor} (R (F) \underset{˙}{\lor} R (G \circ F^{-1}))$
43	6 7	ltrnco	$⊢ ((K \in HL \land W \in H) \land G \in T \land F^{-1} \in T) \to G \circ F^{-1} \in T$
44	12 13 35 43	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to G \circ F^{-1} \in T$
45	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T) \to R (G \circ F^{-1}) \in B$
46	12 44 45	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \in B$
47	1 3	latjass	$⊢ (K \in Lat \land (P \in B \land R (G) \in B \land R (G \circ F^{-1}) \in B)) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\lor} R (G \circ F^{-1}) = P \underset{˙}{\lor} (R (G) \underset{˙}{\lor} R (G \circ F^{-1}))$
48	19 22 24 46 47	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\lor} R (G \circ F^{-1}) = P \underset{˙}{\lor} (R (G) \underset{˙}{\lor} R (G \circ F^{-1}))$
49	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in B$
50	12 14 49	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to R (F) \in B$
51	1 3	latjass	$⊢ (K \in Lat \land (P \in B \land R (F) \in B \land R (G \circ F^{-1}) \in B)) \to (P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1}) = P \underset{˙}{\lor} (R (F) \underset{˙}{\lor} R (G \circ F^{-1}))$
52	19 22 50 46 51	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1}) = P \underset{˙}{\lor} (R (F) \underset{˙}{\lor} R (G \circ F^{-1}))$
53	42 48 52	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\lor} R (G \circ F^{-1}) = (P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})$
54	53	oveq1d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
55		simp3l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))$
56	1 5	atbase	$⊢ Q \in A \to Q \in B$
57	27 56	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to Q \in B$
58	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land R (F) \in B) \to P \underset{˙}{\lor} R (F) \in B$
59	19 22 50 58	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to P \underset{˙}{\lor} R (F) \in B$
60	1 2 3	latjlej1	$⊢ (K \in Lat \land (Q \in B \land P \underset{˙}{\lor} R (F) \in B \land R (G \circ F^{-1}) \in B)) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \to (Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})))$
61	19 57 59 46 60	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \to (Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})))$
62	55 61	mpd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to (Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1}))$
63	1 3	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} R (F) \in B \land R (G \circ F^{-1}) \in B) \to (P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
64	19 59 46 63	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
65	1 2 4	latleeqm2	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R (G \circ F^{-1}) \in B \land (P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1}) \in B) \to ((Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})) \leftrightarrow ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = Q \underset{˙}{\lor} R (G \circ F^{-1}))$
66	19 29 64 65	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to ((Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\leq} ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})) \leftrightarrow ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = Q \underset{˙}{\lor} R (G \circ F^{-1}))$
67	62 66	mpbid	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to ((P \underset{˙}{\lor} R (F)) \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = Q \underset{˙}{\lor} R (G \circ F^{-1})$
68	33 54 67	3eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\lor} R (G \circ F^{-1}) = Q \underset{˙}{\lor} R (G \circ F^{-1})$
69	10 68	eqtrid	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land (P \in A \land Q \in A) \land (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \land R (F) \neq R (G))) \to S \underset{˙}{\lor} R (G \circ F^{-1}) = Q \underset{˙}{\lor} R (G \circ F^{-1})$

Metamath Proof Explorer

Theorem cdlemh1

Proof