llnexchb2lem

	Ref	Expression
Hypotheses	llnexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llnexch.j	$⊢ \underset{˙}{\lor} = join (K)$
	llnexch.m	$⊢ \underset{˙}{\land} = meet (K)$
	llnexch.a	$⊢ A = Atoms (K)$
	llnexch.n	$⊢ N = LLines (K)$
Assertion	llnexchb2lem	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (P \underset{˙}{\lor} Q))$

Proof

Step	Hyp	Ref	Expression
1		llnexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llnexch.j	$⊢ \underset{˙}{\lor} = join (K)$
3		llnexch.m	$⊢ \underset{˙}{\land} = meet (K)$
4		llnexch.a	$⊢ A = Atoms (K)$
5		llnexch.n	$⊢ N = LLines (K)$
6		simpl11	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in HL$
7		simpl21	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in A$
8		simpl12	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \in N$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 5	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
11	8 10	syl	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \in {Base}_{K}$
12	6	hllatd	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in Lat$
13		simpl13	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Y \in N$
14	9 5	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
15	13 14	syl	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Y \in {Base}_{K}$
16	9 3	latmcl	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to X \underset{˙}{\land} Y \in {Base}_{K}$
17	12 11 15 16	syl3anc	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} Y \in {Base}_{K}$
18	9 1 3	latmle1	$⊢ (K \in Lat \land X \in {Base}_{K} \land Y \in {Base}_{K}) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
19	12 11 15 18	syl3anc	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} X$
20	9 1 2 3 4	atmod2i2	$⊢ (K \in HL \land (P \in A \land X \in {Base}_{K} \land X \underset{˙}{\land} Y \in {Base}_{K}) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} X) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X \underset{˙}{\land} (P \underset{˙}{\lor} (X \underset{˙}{\land} Y))$
21	6 7 11 17 19 20	syl131anc	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X \underset{˙}{\land} (P \underset{˙}{\lor} (X \underset{˙}{\land} Y))$
22	9 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
23	7 22	syl	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in {Base}_{K}$
24	9 3	latmcom	$⊢ (K \in Lat \land X \in {Base}_{K} \land P \in {Base}_{K}) \to X \underset{˙}{\land} P = P \underset{˙}{\land} X$
25	12 11 23 24	syl3anc	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} P = P \underset{˙}{\land} X$
26		simpl23	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg P \underset{˙}{\leq} X$
27		hlatl	$⊢ K \in HL \to K \in AtLat$
28	6 27	syl	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in AtLat$
29		eqid	$⊢ 0. (K) = 0. (K)$
30	9 1 3 29 4	atnle	$⊢ (K \in AtLat \land P \in A \land X \in {Base}_{K}) \to (\neg P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\land} X = 0. (K))$
31	28 7 11 30	syl3anc	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (\neg P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\land} X = 0. (K))$
32	26 31	mpbid	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\land} X = 0. (K)$
33	25 32	eqtrd	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} P = 0. (K)$
34	33	oveq1d	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (X \underset{˙}{\land} P) \underset{˙}{\lor} (X \underset{˙}{\land} Y) = 0. (K) \underset{˙}{\lor} (X \underset{˙}{\land} Y)$
35		simpr	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
36		hlcvl	$⊢ K \in HL \to K \in CvLat$
37	6 36	syl	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in CvLat$
38		simpl3	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} Y \in A$
39		simpl22	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in A$
40		breq1	$⊢ P = X \underset{˙}{\land} Y \to (P \underset{˙}{\leq} X \leftrightarrow (X \underset{˙}{\land} Y) \underset{˙}{\leq} X)$
41	19 40	syl5ibrcom	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P = X \underset{˙}{\land} Y \to P \underset{˙}{\leq} X)$
42	41	necon3bd	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (\neg P \underset{˙}{\leq} X \to P \neq X \underset{˙}{\land} Y)$
43	26 42	mpd	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq X \underset{˙}{\land} Y$
44	43	necomd	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} Y \neq P$
45	1 2 4	cvlatexchb1	$⊢ (K \in CvLat \land (X \underset{˙}{\land} Y \in A \land Q \in A \land P \in A) \land X \underset{˙}{\land} Y \neq P) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow P \underset{˙}{\lor} (X \underset{˙}{\land} Y) = P \underset{˙}{\lor} Q)$
46	37 38 39 7 44 45	syl131anc	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow P \underset{˙}{\lor} (X \underset{˙}{\land} Y) = P \underset{˙}{\lor} Q)$
47	35 46	mpbid	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} (X \underset{˙}{\land} Y) = P \underset{˙}{\lor} Q$
48	47	oveq2d	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} (P \underset{˙}{\lor} (X \underset{˙}{\land} Y)) = X \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
49	21 34 48	3eqtr3rd	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} (P \underset{˙}{\lor} Q) = 0. (K) \underset{˙}{\lor} (X \underset{˙}{\land} Y)$
50		hlol	$⊢ K \in HL \to K \in OL$
51	6 50	syl	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in OL$
52	9 2 29	olj02	$⊢ (K \in OL \land X \underset{˙}{\land} Y \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X \underset{˙}{\land} Y$
53	51 17 52	syl2anc	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to 0. (K) \underset{˙}{\lor} (X \underset{˙}{\land} Y) = X \underset{˙}{\land} Y$
54	49 53	eqtr2d	$⊢ (((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \land (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to X \underset{˙}{\land} Y = X \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
55	54	ex	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to X \underset{˙}{\land} Y = X \underset{˙}{\land} (P \underset{˙}{\lor} Q))$
56		simp11	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to K \in HL$
57	56	hllatd	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to K \in Lat$
58		simp12	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to X \in N$
59	58 10	syl	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to X \in {Base}_{K}$
60		simp21	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to P \in A$
61		simp22	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to Q \in A$
62	9 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
63	56 60 61 62	syl3anc	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
64	9 1 3	latmle2	$⊢ (K \in Lat \land X \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (X \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
65	57 59 63 64	syl3anc	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to (X \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
66		breq1	$⊢ X \underset{˙}{\land} Y = X \underset{˙}{\land} (P \underset{˙}{\lor} Q) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow (X \underset{˙}{\land} (P \underset{˙}{\lor} Q)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
67	65 66	syl5ibrcom	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to (X \underset{˙}{\land} Y = X \underset{˙}{\land} (P \underset{˙}{\lor} Q) \to (X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
68	55 67	impbid	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (P \in A \land Q \in A \land \neg P \underset{˙}{\leq} X) \land X \underset{˙}{\land} Y \in A) \to ((X \underset{˙}{\land} Y) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow X \underset{˙}{\land} Y = X \underset{˙}{\land} (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer

Theorem llnexchb2lem

Proof