cvrat4

Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in PtakPulmannova p. 68. Also Lemma 9.2(delta) in MaedaMaeda p. 41. ( atcvat4i analog.) (Contributed by NM, 30-Nov-2011)

	Ref	Expression
Hypotheses	cvrat4.b	$⊢ B = {Base}_{K}$
	cvrat4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvrat4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvrat4.z	$⊢ \underset{˙}{0} = 0. (K)$
	cvrat4.a	$⊢ A = Atoms (K)$
Assertion	cvrat4	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq \underset{˙}{0} \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$

Proof

Step	Hyp	Ref	Expression
1		cvrat4.b	$⊢ B = {Base}_{K}$
2		cvrat4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrat4.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvrat4.z	$⊢ \underset{˙}{0} = 0. (K)$
5		cvrat4.a	$⊢ A = Atoms (K)$
6		hlatl	$⊢ K \in HL \to K \in AtLat$
7	6	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in AtLat$
8		simpr1	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to X \in B$
9	1 2 4 5	atlex	$⊢ (K \in AtLat \land X \in B \land X \neq \underset{˙}{0}) \to \exists r \in A r \underset{˙}{\leq} X$
10	9	3exp	$⊢ K \in AtLat \to (X \in B \to (X \neq \underset{˙}{0} \to \exists r \in A r \underset{˙}{\leq} X))$
11	7 8 10	sylc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X \neq \underset{˙}{0} \to \exists r \in A r \underset{˙}{\leq} X)$
12	11	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land P = Q) \to (X \neq \underset{˙}{0} \to \exists r \in A r \underset{˙}{\leq} X)$
13		simpll	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land r \in A) \to K \in HL$
14		simplr3	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land r \in A) \to Q \in A$
15		simpr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land r \in A) \to r \in A$
16	2 3 5	hlatlej1	$⊢ (K \in HL \land Q \in A \land r \in A) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} r)$
17	13 14 15 16	syl3anc	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land r \in A) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} r)$
18		breq1	$⊢ P = Q \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} r) \leftrightarrow Q \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
19	17 18	syl5ibr	$⊢ P = Q \to (((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land r \in A) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
20	19	expd	$⊢ P = Q \to ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (r \in A \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$
21	20	impcom	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land P = Q) \to (r \in A \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
22	21	anim2d	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land P = Q) \to ((r \underset{˙}{\leq} X \land r \in A) \to (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$
23	22	expcomd	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land P = Q) \to (r \in A \to (r \underset{˙}{\leq} X \to (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
24	23	reximdvai	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land P = Q) \to (\exists r \in A r \underset{˙}{\leq} X \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$
25	12 24	syld	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land P = Q) \to (X \neq \underset{˙}{0} \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$
26	25	ex	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (P = Q \to (X \neq \underset{˙}{0} \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
27	26	a1i	$⊢ P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (P = Q \to (X \neq \underset{˙}{0} \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))))$
28	27	com4l	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (P = Q \to (X \neq \underset{˙}{0} \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))))$
29	28	imp4a	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (P = Q \to ((X \neq \underset{˙}{0} \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
30		hllat	$⊢ K \in HL \to K \in Lat$
31	30	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in Lat$
32		simpr3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \in A$
33	1 5	atbase	$⊢ Q \in A \to Q \in B$
34	32 33	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q \in B$
35	1 2 3	latleeqj2	$⊢ (K \in Lat \land Q \in B \land X \in B) \to (Q \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\lor} Q = X)$
36	31 34 8 35	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (Q \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\lor} Q = X)$
37	36	biimpa	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land Q \underset{˙}{\leq} X) \to X \underset{˙}{\lor} Q = X$
38	37	breq2d	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land Q \underset{˙}{\leq} X) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \leftrightarrow P \underset{˙}{\leq} X)$
39	38	biimpa	$⊢ (((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to P \underset{˙}{\leq} X$
40	39	expl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((Q \underset{˙}{\leq} X \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to P \underset{˙}{\leq} X)$
41		simpl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in HL$
42		simpr2	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \in A$
43	2 3 5	hlatlej2	$⊢ (K \in HL \land Q \in A \land P \in A) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
44	41 32 42 43	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
45	40 44	jctird	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((Q \underset{˙}{\leq} X \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} P)))$
46	45 42	jctild	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((Q \underset{˙}{\leq} X \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to (P \in A \land (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} P))))$
47	46	impl	$⊢ (((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to (P \in A \land (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} P)))$
48		breq1	$⊢ r = P \to (r \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\leq} X)$
49		oveq2	$⊢ r = P \to Q \underset{˙}{\lor} r = Q \underset{˙}{\lor} P$
50	49	breq2d	$⊢ r = P \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} r) \leftrightarrow P \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
51	48 50	anbi12d	$⊢ r = P \to ((r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)) \leftrightarrow (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} P)))$
52	51	rspcev	$⊢ (P \in A \land (P \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} P))) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
53	47 52	syl	$⊢ (((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
54	53	adantrl	$⊢ (((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land Q \underset{˙}{\leq} X) \land (X \neq \underset{˙}{0} \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
55	54	exp31	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (Q \underset{˙}{\leq} X \to ((X \neq \underset{˙}{0} \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
56		simpr	$⊢ (X \neq \underset{˙}{0} \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
57		ioran	$⊢ \neg (P = Q \lor Q \underset{˙}{\leq} X) \leftrightarrow (\neg P = Q \land \neg Q \underset{˙}{\leq} X)$
58		df-ne	$⊢ P \neq Q \leftrightarrow \neg P = Q$
59	58	anbi1i	$⊢ (P \neq Q \land \neg Q \underset{˙}{\leq} X) \leftrightarrow (\neg P = Q \land \neg Q \underset{˙}{\leq} X)$
60	57 59	bitr4i	$⊢ \neg (P = Q \lor Q \underset{˙}{\leq} X) \leftrightarrow (P \neq Q \land \neg Q \underset{˙}{\leq} X)$
61		eqid	$⊢ meet (K) = meet (K)$
62	1 2 3 61 5	cvrat3	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((P \neq Q \land \neg Q \underset{˙}{\leq} X \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to X meet (K) (P \underset{˙}{\lor} Q) \in A)$
63	62	3expd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (P \neq Q \to (\neg Q \underset{˙}{\leq} X \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to X meet (K) (P \underset{˙}{\lor} Q) \in A)))$
64	63	imp4c	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to X meet (K) (P \underset{˙}{\lor} Q) \in A)$
65	1 5	atbase	$⊢ P \in A \to P \in B$
66	42 65	syl	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \in B$
67	1 3	latjcl	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q \in B$
68	31 66 34 67	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \underset{˙}{\lor} Q \in B$
69	1 2 61	latmle1	$⊢ (K \in Lat \land X \in B \land P \underset{˙}{\lor} Q \in B) \to (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X$
70	31 8 68 69	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X$
71	70	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X$
72		simpll	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to K \in HL$
73	63	imp44	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to X meet (K) (P \underset{˙}{\lor} Q) \in A$
74		simplr2	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to P \in A$
75	34	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to Q \in B$
76	73 74 75	3jca	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)$
77	72 76	jca	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B))$
78	1 2 61 4 5	atnle	$⊢ (K \in AtLat \land Q \in A \land X \in B) \to (\neg Q \underset{˙}{\leq} X \leftrightarrow Q meet (K) X = \underset{˙}{0})$
79	7 32 8 78	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (\neg Q \underset{˙}{\leq} X \leftrightarrow Q meet (K) X = \underset{˙}{0})$
80	1 61	latmcom	$⊢ (K \in Lat \land Q \in B \land X \in B) \to Q meet (K) X = X meet (K) Q$
81	31 34 8 80	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q meet (K) X = X meet (K) Q$
82	81	eqeq1d	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (Q meet (K) X = \underset{˙}{0} \leftrightarrow X meet (K) Q = \underset{˙}{0})$
83	79 82	bitrd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (\neg Q \underset{˙}{\leq} X \leftrightarrow X meet (K) Q = \underset{˙}{0})$
84	1 61	latmcl	$⊢ (K \in Lat \land X \in B \land P \underset{˙}{\lor} Q \in B) \to X meet (K) (P \underset{˙}{\lor} Q) \in B$
85	31 8 68 84	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to X meet (K) (P \underset{˙}{\lor} Q) \in B$
86	85 8 34	3jca	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X meet (K) (P \underset{˙}{\lor} Q) \in B \land X \in B \land Q \in B)$
87	31 86	jca	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (K \in Lat \land (X meet (K) (P \underset{˙}{\lor} Q) \in B \land X \in B \land Q \in B))$
88	1 2 61	latmlem2	$⊢ (K \in Lat \land (X meet (K) (P \underset{˙}{\lor} Q) \in B \land X \in B \land Q \in B)) \to ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X \to (Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} (Q meet (K) X))$
89	87 70 88	sylc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} (Q meet (K) X)$
90	89 81	breqtrd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} (X meet (K) Q)$
91		breq2	$⊢ X meet (K) Q = \underset{˙}{0} \to ((Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} (X meet (K) Q) \leftrightarrow (Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} \underset{˙}{0})$
92	90 91	syl5ibcom	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X meet (K) Q = \underset{˙}{0} \to (Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} \underset{˙}{0})$
93		hlop	$⊢ K \in HL \to K \in OP$
94	93	adantr	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to K \in OP$
95	1 61	latmcl	$⊢ (K \in Lat \land Q \in B \land X meet (K) (P \underset{˙}{\lor} Q) \in B) \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) \in B$
96	31 34 85 95	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) \in B$
97	1 2 4	ople0	$⊢ (K \in OP \land Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) \in B) \to ((Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} \underset{˙}{0} \leftrightarrow Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0})$
98	94 96 97	syl2anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q))) \underset{˙}{\leq} \underset{˙}{0} \leftrightarrow Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0})$
99	92 98	sylibd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X meet (K) Q = \underset{˙}{0} \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0})$
100	83 99	sylbid	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (\neg Q \underset{˙}{\leq} X \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0})$
101	100	imp	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land \neg Q \underset{˙}{\leq} X) \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0}$
102	101	adantrl	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land (P \neq Q \land \neg Q \underset{˙}{\leq} X)) \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0}$
103	102	adantrr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0}$
104	1 2 61	latmle2	$⊢ (K \in Lat \land X \in B \land P \underset{˙}{\lor} Q \in B) \to (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
105	31 8 68 104	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
106	1 3	latjcom	$⊢ (K \in Lat \land P \in B \land Q \in B) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
107	31 66 34 106	syl3anc	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
108	105 107	breqtrd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
109	108	adantr	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
110	30	adantr	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to K \in Lat$
111		simpr3	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to Q \in B$
112		simpr1	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to X meet (K) (P \underset{˙}{\lor} Q) \in A$
113	1 5	atbase	$⊢ X meet (K) (P \underset{˙}{\lor} Q) \in A \to X meet (K) (P \underset{˙}{\lor} Q) \in B$
114	112 113	syl	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to X meet (K) (P \underset{˙}{\lor} Q) \in B$
115	1 61	latmcom	$⊢ (K \in Lat \land Q \in B \land X meet (K) (P \underset{˙}{\lor} Q) \in B) \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = (X meet (K) (P \underset{˙}{\lor} Q)) meet (K) Q$
116	110 111 114 115	syl3anc	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = (X meet (K) (P \underset{˙}{\lor} Q)) meet (K) Q$
117	116	eqeq1d	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to (Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0} \leftrightarrow (X meet (K) (P \underset{˙}{\lor} Q)) meet (K) Q = \underset{˙}{0})$
118	1 2 3 61 4 5	hlexch3	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B) \land (X meet (K) (P \underset{˙}{\lor} Q)) meet (K) Q = \underset{˙}{0}) \to ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q))))$
119	118	3expia	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to ((X meet (K) (P \underset{˙}{\lor} Q)) meet (K) Q = \underset{˙}{0} \to ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q)))))$
120	117 119	sylbid	$⊢ (K \in HL \land (X meet (K) (P \underset{˙}{\lor} Q) \in A \land P \in A \land Q \in B)) \to (Q meet (K) (X meet (K) (P \underset{˙}{\lor} Q)) = \underset{˙}{0} \to ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q)))))$
121	77 103 109 120	syl3c	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q)))$
122	71 121	jca	$⊢ ((K \in HL \land (X \in B \land P \in A \land Q \in A)) \land ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))) \to ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q))))$
123	122	ex	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q)))))$
124	64 123	jcad	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to (X meet (K) (P \underset{˙}{\lor} Q) \in A \land ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q))))))$
125		breq1	$⊢ r = X meet (K) (P \underset{˙}{\lor} Q) \to (r \underset{˙}{\leq} X \leftrightarrow (X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X)$
126		oveq2	$⊢ r = X meet (K) (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\lor} r = Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q))$
127	126	breq2d	$⊢ r = X meet (K) (P \underset{˙}{\lor} Q) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} r) \leftrightarrow P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q))))$
128	125 127	anbi12d	$⊢ r = X meet (K) (P \underset{˙}{\lor} Q) \to ((r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)) \leftrightarrow ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q)))))$
129	128	rspcev	$⊢ (X meet (K) (P \underset{˙}{\lor} Q) \in A \land ((X meet (K) (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} (X meet (K) (P \underset{˙}{\lor} Q))))) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))$
130	124 129	syl6	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (((P \neq Q \land \neg Q \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$
131	130	expd	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((P \neq Q \land \neg Q \underset{˙}{\leq} X) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
132	60 131	syl5bi	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (\neg (P = Q \lor Q \underset{˙}{\leq} X) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
133	56 132	syl7	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to (\neg (P = Q \lor Q \underset{˙}{\leq} X) \to ((X \neq \underset{˙}{0} \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r))))$
134	29 55 133	ecase3d	$⊢ (K \in HL \land (X \in B \land P \in A \land Q \in A)) \to ((X \neq \underset{˙}{0} \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to \exists r \in A (r \underset{˙}{\leq} X \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} r)))$

Metamath Proof Explorer

Theorem cvrat4

Proof