cdlemh2

Description: Part of proof of Lemma H of Crawley p. 118. (Contributed by NM, 16-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}))$
	cdlemh.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	cdlemh2	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to S \underset{˙}{\land} W = \underset{˙}{0}$

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		cdlemh.z	$⊢ \underset{˙}{0} = 0. (K)$
11	9	oveq1i	$⊢ S \underset{˙}{\land} W = ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\land} W$
12		simp11l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in HL$
13		hlol	$⊢ K \in HL \to K \in OL$
14	12 13	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in OL$
15	12	hllatd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in Lat$
16		simp2ll	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \in A$
17	1 5	atbase	$⊢ P \in A \to P \in B$
18	16 17	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \in B$
19		simp11r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to W \in H$
20	12 19	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (K \in HL \land W \in H)$
21		simp13	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \in T$
22	1 6 7 8	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in B$
23	20 21 22	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \in B$
24	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land R (G) \in B) \to P \underset{˙}{\lor} R (G) \in B$
25	15 18 23 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \underset{˙}{\lor} R (G) \in B$
26		simp2rl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to Q \in A$
27	1 5	atbase	$⊢ Q \in A \to Q \in B$
28	26 27	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to Q \in B$
29		simp12	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F \in T$
30	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
31	20 29 30	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F^{-1} \in T$
32	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$
33	20 21 31 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \circ F^{-1} \in T$
34	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$
35	20 33 34	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \in B$
36	1 3	latjcl	$⊢ (K \in Lat \land Q \in B \land R (G \circ F^{-1}) \in B) \to Q \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
37	15 28 35 36	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to Q \underset{˙}{\lor} R (G \circ F^{-1}) \in B$
38	1 6	lhpbase	$⊢ W \in H \to W \in B$
39	19 38	syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to W \in B$
40	1 4	latmassOLD	$⊢ (K \in OL \land (P \underset{˙}{\lor} R (G) \in B \land Q \underset{˙}{\lor} R (G \circ F^{-1}) \in B \land W \in B)) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\land} W = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} ((Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} W)$
41	14 25 37 39 40	syl13anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\land} W = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} ((Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} W)$
42		simp2r	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
43	2 4 10 5 6	lhpmat	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Q \underset{˙}{\land} W = \underset{˙}{0}$
44	20 42 43	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to Q \underset{˙}{\land} W = \underset{˙}{0}$
45	44	oveq1d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (Q \underset{˙}{\land} W) \underset{˙}{\lor} R (G \circ F^{-1}) = \underset{˙}{0} \underset{˙}{\lor} R (G \circ F^{-1})$
46	2 6 7 8	trlle	$⊢ ((K \in HL \land W \in H) \land G \circ F^{-1} \in T) \to R (G \circ F^{-1}) \underset{˙}{\leq} W$
47	20 33 46	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \underset{˙}{\leq} W$
48	1 2 3 4 5	atmod4i2	$⊢ (K \in HL \land (Q \in A \land R (G \circ F^{-1}) \in B \land W \in B) \land R (G \circ F^{-1}) \underset{˙}{\leq} W) \to (Q \underset{˙}{\land} W) \underset{˙}{\lor} R (G \circ F^{-1}) = (Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} W$
49	12 26 35 39 47 48	syl131anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (Q \underset{˙}{\land} W) \underset{˙}{\lor} R (G \circ F^{-1}) = (Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} W$
50	1 3 10	olj02	$⊢ (K \in OL \land R (G \circ F^{-1}) \in B) \to \underset{˙}{0} \underset{˙}{\lor} R (G \circ F^{-1}) = R (G \circ F^{-1})$
51	14 35 50	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to \underset{˙}{0} \underset{˙}{\lor} R (G \circ F^{-1}) = R (G \circ F^{-1})$
52	45 49 51	3eqtr3rd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) = (Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} W$
53	52	oveq2d	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} R (G \circ F^{-1}) = (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} ((Q \underset{˙}{\lor} R (G \circ F^{-1})) \underset{˙}{\land} W)$
54		simp2l	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
55	21 31	jca	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (G \in T \land F^{-1} \in T)$
56		simp33	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (F) \neq R (G)$
57	56	necomd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \neq R (F)$
58	6 7 8	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
59	20 29 58	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (F^{-1}) = R (F)$
60	57 59	neeqtrrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \neq R (F^{-1})$
61		simp31	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F \neq {I ↾}_{B}$
62	1 6 7	ltrncnvnid	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to F^{-1} \neq {I ↾}_{B}$
63	20 29 61 62	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F^{-1} \neq {I ↾}_{B}$
64	1 6 7 8	trlcone	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F^{-1} \in T) \land (R (G) \neq R (F^{-1}) \land F^{-1} \neq {I ↾}_{B})) \to R (G) \neq R (G \circ F^{-1})$
65	20 55 60 63 64	syl112anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \neq R (G \circ F^{-1})$
66		simp32	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \neq {I ↾}_{B}$
67	1 5 6 7 8	trlnidat	$⊢ ((K \in HL \land W \in H) \land G \in T \land G \neq {I ↾}_{B}) \to R (G) \in A$
68	20 21 66 67	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \in A$
69	2 6 7 8	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
70	20 21 69	syl2anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \underset{˙}{\leq} W$
71	5 6 7 8	trlcoat	$⊢ ((K \in HL \land W \in H) \land (G \in T \land F^{-1} \in T) \land R (G) \neq R (F^{-1})) \to R (G \circ F^{-1}) \in A$
72	20 55 60 71	syl3anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \in A$
73	2 3 4 10 5 6	lhp2at0	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land R (G) \neq R (G \circ F^{-1})) \land (R (G) \in A \land R (G) \underset{˙}{\leq} W) \land (R (G \circ F^{-1}) \in A \land R (G \circ F^{-1}) \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} R (G \circ F^{-1}) = \underset{˙}{0}$
74	20 54 65 68 70 72 47 73	syl322anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} R (G \circ F^{-1}) = \underset{˙}{0}$
75	41 53 74	3eqtr2rd	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to \underset{˙}{0} = ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \underset{˙}{\land} W$
76	11 75	eqtr4id	$⊢ (((K \in HL \land W \in H) \land F \in T \land G \in T) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to S \underset{˙}{\land} W = \underset{˙}{0}$

Metamath Proof Explorer

Theorem cdlemh2

Proof