cdlemh

	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	cdlemh	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$

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		simp1	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to ((K \in HL \land W \in H) \land F \in T \land G \in T)$
11		simp21l	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \in A$
12		simp22l	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to Q \in A$
13		simp23	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))$
14		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (F) \neq R (G)$
15	1 2 3 4 5 6 7 8 9	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})$
16	10 11 12 13 14 15	syl122anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to S \underset{˙}{\lor} R (G \circ F^{-1}) = Q \underset{˙}{\lor} R (G \circ F^{-1})$
17		oveq1	$⊢ S = 0. (K) \to S \underset{˙}{\lor} R (G \circ F^{-1}) = 0. (K) \underset{˙}{\lor} R (G \circ F^{-1})$
18		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in HL$
19		hlol	$⊢ K \in HL \to K \in OL$
20	18 19	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to K \in OL$
21		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to W \in H$
22	18 21	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (K \in HL \land W \in H)$
23		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \in T$
24		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F \in T$
25	6 7	ltrncnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F^{-1} \in T$
26	22 24 25	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F^{-1} \in T$
27	23 26	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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)$
28	14	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \neq R (F)$
29	6 7 8	trlcnv	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F^{-1}) = R (F)$
30	22 24 29	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (F^{-1}) = R (F)$
31	28 30	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \neq R (F^{-1})$
32	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$
33	22 27 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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \in A$
34	1 5	atbase	$⊢ R (G \circ F^{-1}) \in A \to R (G \circ F^{-1}) \in B$
35	33 34	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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		eqid	$⊢ 0. (K) = 0. (K)$
37	1 3 36	olj02	$⊢ (K \in OL \land R (G \circ F^{-1}) \in B) \to 0. (K) \underset{˙}{\lor} R (G \circ F^{-1}) = R (G \circ F^{-1})$
38	20 35 37	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to 0. (K) \underset{˙}{\lor} R (G \circ F^{-1}) = R (G \circ F^{-1})$
39	17 38	sylan9eqr	$⊢ ((((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \land S = 0. (K)) \to S \underset{˙}{\lor} R (G \circ F^{-1}) = R (G \circ F^{-1})$
40	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$
41	22 23 26 40	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \circ F^{-1} \in T$
42	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$
43	22 41 42	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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$
44		simp22r	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to \neg Q \underset{˙}{\leq} W$
45		nbrne2	$⊢ (R (G \circ F^{-1}) \underset{˙}{\leq} W \land \neg Q \underset{˙}{\leq} W) \to R (G \circ F^{-1}) \neq Q$
46	45	necomd	$⊢ (R (G \circ F^{-1}) \underset{˙}{\leq} W \land \neg Q \underset{˙}{\leq} W) \to Q \neq R (G \circ F^{-1})$
47	43 44 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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to Q \neq R (G \circ F^{-1})$
48		eqid	$⊢ LLines (K) = LLines (K)$
49	3 5 48	llni2	$⊢ ((K \in HL \land Q \in A \land R (G \circ F^{-1}) \in A) \land Q \neq R (G \circ F^{-1})) \to Q \underset{˙}{\lor} R (G \circ F^{-1}) \in LLines (K)$
50	18 12 33 47 49	syl31anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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 LLines (K)$
51	5 48	llnneat	$⊢ (K \in HL \land Q \underset{˙}{\lor} R (G \circ F^{-1}) \in LLines (K)) \to \neg Q \underset{˙}{\lor} R (G \circ F^{-1}) \in A$
52	18 50 51	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to \neg Q \underset{˙}{\lor} R (G \circ F^{-1}) \in A$
53		nelne2	$⊢ (R (G \circ F^{-1}) \in A \land \neg Q \underset{˙}{\lor} R (G \circ F^{-1}) \in A) \to R (G \circ F^{-1}) \neq Q \underset{˙}{\lor} R (G \circ F^{-1})$
54	33 52 53	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \neq Q \underset{˙}{\lor} R (G \circ F^{-1})$
55	54	adantr	$⊢ ((((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \land S = 0. (K)) \to R (G \circ F^{-1}) \neq Q \underset{˙}{\lor} R (G \circ F^{-1})$
56	39 55	eqnetrd	$⊢ ((((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \land S = 0. (K)) \to S \underset{˙}{\lor} R (G \circ F^{-1}) \neq Q \underset{˙}{\lor} R (G \circ F^{-1})$
57	56	ex	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (S = 0. (K) \to S \underset{˙}{\lor} R (G \circ F^{-1}) \neq Q \underset{˙}{\lor} R (G \circ F^{-1}))$
58	57	necon2d	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (S \underset{˙}{\lor} R (G \circ F^{-1}) = Q \underset{˙}{\lor} R (G \circ F^{-1}) \to S \neq 0. (K))$
59	16 58	mpd	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to S \neq 0. (K)$
60		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to G \neq {I ↾}_{B}$
61	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$
62	22 23 60 61	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \in A$
63	2 3 5	hlatlej2	$⊢ (K \in HL \land P \in A \land R (G) \in A) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
64	18 11 62 63	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G))$
65		simp22	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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)$
66		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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F \neq {I ↾}_{B}$
67	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}$
68	22 24 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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to F^{-1} \neq {I ↾}_{B}$
69	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})$
70	69	necomd	$⊢ ((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 \circ F^{-1}) \neq R (G)$
71	22 23 26 31 68 70	syl122anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G \circ F^{-1}) \neq R (G)$
72	2 6 7 8	trlle	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \underset{˙}{\leq} W$
73	22 23 72	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to R (G) \underset{˙}{\leq} W$
74	2 3 5 6	lhp2atnle	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land R (G \circ F^{-1}) \neq R (G)) \land (R (G \circ F^{-1}) \in A \land R (G \circ F^{-1}) \underset{˙}{\leq} W) \land (R (G) \in A \land R (G) \underset{˙}{\leq} W)) \to \neg R (G) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
75	22 65 71 33 43 62 73 74	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to \neg R (G) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (G \circ F^{-1}))$
76		nbrne1	$⊢ (R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} R (G)) \land \neg R (G) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (G \circ F^{-1}))) \to P \underset{˙}{\lor} R (G) \neq Q \underset{˙}{\lor} R (G \circ F^{-1})$
77	64 75 76	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to P \underset{˙}{\lor} R (G) \neq Q \underset{˙}{\lor} R (G \circ F^{-1})$
78	3 4 36 5	2atmat0	$⊢ ((K \in HL \land P \in A \land R (G) \in A) \land (Q \in A \land R (G \circ F^{-1}) \in A \land P \underset{˙}{\lor} R (G) \neq Q \underset{˙}{\lor} R (G \circ F^{-1}))) \to ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) \in A \lor (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = 0. (K))$
79	18 11 62 12 33 77 78	syl33anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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})) \in A \lor (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = 0. (K))$
80	9	eleq1i	$⊢ S \in A \leftrightarrow (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) \in A$
81	9	eqeq1i	$⊢ S = 0. (K) \leftrightarrow (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = 0. (K)$
82	80 81	orbi12i	$⊢ (S \in A \lor S = 0. (K)) \leftrightarrow ((P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) \in A \lor (P \underset{˙}{\lor} R (G)) \underset{˙}{\land} (Q \underset{˙}{\lor} R (G \circ F^{-1})) = 0. (K))$
83	79 82	sylibr	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (S \in A \lor S = 0. (K))$
84	83	ord	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (\neg S \in A \to S = 0. (K))$
85	84	necon1ad	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (S \neq 0. (K) \to S \in A)$
86	59 85	mpd	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to S \in A$
87		simp21	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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)$
88	87 65	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \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) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
89	1 2 3 4 5 6 7 8 9 36	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 = 0. (K)$
90	88 89	syld3an2	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to S \underset{˙}{\land} W = 0. (K)$
91	2 4 36 5 6	lhpmatb	$⊢ ((K \in HL \land W \in H) \land S \in A) \to (\neg S \underset{˙}{\leq} W \leftrightarrow S \underset{˙}{\land} W = 0. (K))$
92	18 21 86 91	syl21anc	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (\neg S \underset{˙}{\leq} W \leftrightarrow S \underset{˙}{\land} W = 0. (K))$
93	90 92	mpbird	$⊢ (((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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to \neg S \underset{˙}{\leq} W$
94	86 93	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 Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))) \land (F \neq {I ↾}_{B} \land G \neq {I ↾}_{B} \land R (F) \neq R (G))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem cdlemh

Proof