cdlemg12e

	Ref	Expression
Hypotheses	cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg12.a	$⊢ A = Atoms (K)$
	cdlemg12.h	$⊢ H = LHyp (K)$
	cdlemg12.t	$⊢ T = LTrn (K) (W)$
	cdlemg12b.r	$⊢ R = trL (K) (W)$
	cdlemg12e.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	cdlemg12e	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		cdlemg12e.z	$⊢ \underset{˙}{0} = 0. (K)$
9		simp33	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to R (F) \neq R (G)$
10		simpl1	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))$
11		simpl21	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to F \in T$
12		simpl22	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to G \in T$
13		simpl23	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to P \neq Q$
14		simpl31	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
15		simpl32	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
16	1 2 3 4 5 6 7	cdlemg12d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R (G) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q)))$
17	10 11 12 13 14 15 16	syl123anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (G) \underset{˙}{\leq} (R (F) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q)))$
18		simpr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}$
19	18	oveq2d	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (F) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q)) = R (F) \underset{˙}{\lor} \underset{˙}{0}$
20		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to K \in HL$
21	20	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to K \in HL$
22		hlol	$⊢ K \in HL \to K \in OL$
23	21 22	syl	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to K \in OL$
24		simpl11	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to (K \in HL \land W \in H)$
25		eqid	$⊢ {Base}_{K} = {Base}_{K}$
26	25 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
27	24 11 26	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (F) \in {Base}_{K}$
28	25 2 8	olj01	$⊢ (K \in OL \land R (F) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} \underset{˙}{0} = R (F)$
29	23 27 28	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (F) \underset{˙}{\lor} \underset{˙}{0} = R (F)$
30	19 29	eqtrd	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (F) \underset{˙}{\lor} ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q)) = R (F)$
31	17 30	breqtrd	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (G) \underset{˙}{\leq} R (F)$
32		hlatl	$⊢ K \in HL \to K \in AtLat$
33	21 32	syl	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to K \in AtLat$
34		hlop	$⊢ K \in HL \to K \in OP$
35	21 34	syl	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to K \in OP$
36	25 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land G \in T) \to R (G) \in {Base}_{K}$
37	24 12 36	syl2anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (G) \in {Base}_{K}$
38		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to P \in A$
39	38	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to P \in A$
40		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to Q \in A$
41	40	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to Q \in A$
42	25 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
43	21 39 41 42	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
44	25 1 8	opnlen0	$⊢ ((K \in OP \land R (G) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R (G) \neq \underset{˙}{0}$
45	35 37 43 15 44	syl31anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (G) \neq \underset{˙}{0}$
46		simp11r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to W \in H$
47	46	adantr	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to W \in H$
48	8 4 5 6 7	trlatn0	$⊢ ((K \in HL \land W \in H) \land G \in T) \to (R (G) \in A \leftrightarrow R (G) \neq \underset{˙}{0})$
49	21 47 12 48	syl21anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to (R (G) \in A \leftrightarrow R (G) \neq \underset{˙}{0})$
50	45 49	mpbird	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (G) \in A$
51	25 1 8	opnlen0	$⊢ ((K \in OP \land R (F) \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R (F) \neq \underset{˙}{0}$
52	35 27 43 14 51	syl31anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (F) \neq \underset{˙}{0}$
53	8 4 5 6 7	trlatn0	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (R (F) \in A \leftrightarrow R (F) \neq \underset{˙}{0})$
54	21 47 11 53	syl21anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to (R (F) \in A \leftrightarrow R (F) \neq \underset{˙}{0})$
55	52 54	mpbird	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (F) \in A$
56	1 4	atcmp	$⊢ (K \in AtLat \land R (G) \in A \land R (F) \in A) \to (R (G) \underset{˙}{\leq} R (F) \leftrightarrow R (G) = R (F))$
57	33 50 55 56	syl3anc	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to (R (G) \underset{˙}{\leq} R (F) \leftrightarrow R (G) = R (F))$
58	31 57	mpbid	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (G) = R (F)$
59	58	eqcomd	$⊢ ((((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \land (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0}) \to R (F) = R (G)$
60	59	ex	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to ((F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) = \underset{˙}{0} \to R (F) = R (G))$
61	60	necon3d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to (R (F) \neq R (G) \to (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) \neq \underset{˙}{0})$
62	9 61	mpd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (F \in T \land G \in T \land P \neq Q) \land (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg R (G) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R (F) \neq R (G))) \to (F (G (P)) \underset{˙}{\lor} P) \underset{˙}{\land} (F (G (Q)) \underset{˙}{\lor} Q) \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem cdlemg12e

Proof