2llnma3r

Description: Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 30-Apr-2013)

	Ref	Expression
Hypotheses	2llnm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	2llnm.j	$⊢ \underset{˙}{\lor} = join (K)$
	2llnm.m	$⊢ \underset{˙}{\land} = meet (K)$
	2llnm.a	$⊢ A = Atoms (K)$
Assertion	2llnma3r	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (Q \underset{˙}{\lor} R) = R$

Proof

Step	Hyp	Ref	Expression
1		2llnm.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		2llnm.j	$⊢ \underset{˙}{\lor} = join (K)$
3		2llnm.m	$⊢ \underset{˙}{\land} = meet (K)$
4		2llnm.a	$⊢ A = Atoms (K)$
5		simp1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to K \in HL$
6		simp21	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to P \in A$
7		simp23	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to R \in A$
8	2 4	hlatjcom	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
9	5 6 7 8	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
10		simp22	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to Q \in A$
11	2 4	hlatjcom	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
12	5 10 7 11	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
13	9 12	oveq12d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (Q \underset{˙}{\lor} R) = (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q)$
14		simpr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to Q = R$
15	14	oveq2d	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to R \underset{˙}{\lor} Q = R \underset{˙}{\lor} R$
16		simpl1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to K \in HL$
17		simpl23	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to R \in A$
18	2 4	hlatjidm	$⊢ (K \in HL \land R \in A) \to R \underset{˙}{\lor} R = R$
19	16 17 18	syl2anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to R \underset{˙}{\lor} R = R$
20	15 19	eqtrd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to R \underset{˙}{\lor} Q = R$
21	20	oveq2d	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) = (R \underset{˙}{\lor} P) \underset{˙}{\land} R$
22	1 2 4	hlatlej1	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} P)$
23	5 7 6 22	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} P)$
24		hllat	$⊢ K \in HL \to K \in Lat$
25	24	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to K \in Lat$
26		eqid	$⊢ {Base}_{K} = {Base}_{K}$
27	26 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
28	7 27	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to R \in {Base}_{K}$
29	26 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land P \in A) \to R \underset{˙}{\lor} P \in {Base}_{K}$
30	5 7 6 29	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to R \underset{˙}{\lor} P \in {Base}_{K}$
31	26 1 3	latleeqm2	$⊢ (K \in Lat \land R \in {Base}_{K} \land R \underset{˙}{\lor} P \in {Base}_{K}) \to (R \underset{˙}{\leq} (R \underset{˙}{\lor} P) \leftrightarrow (R \underset{˙}{\lor} P) \underset{˙}{\land} R = R)$
32	25 28 30 31	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to (R \underset{˙}{\leq} (R \underset{˙}{\lor} P) \leftrightarrow (R \underset{˙}{\lor} P) \underset{˙}{\land} R = R)$
33	23 32	mpbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} R = R$
34	33	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} R = R$
35	21 34	eqtrd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q = R) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) = R$
36		simpl1	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to K \in HL$
37		simpl21	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to P \in A$
38		simpl23	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to R \in A$
39		simpl22	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to Q \in A$
40		simpl3	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R$
41	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land R \in A) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
42	5 6 7 41	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
43	26 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
44	10 43	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to Q \in {Base}_{K}$
45	26 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R \in {Base}_{K}$
46	5 6 7 45	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to P \underset{˙}{\lor} R \in {Base}_{K}$
47	26 1 2	latjle12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K})) \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
48	25 44 28 46 47	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
49	48	biimpd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to ((Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
50	42 49	mpan2d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
51	50	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to (Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
52		simpr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to Q \neq R$
53	1 2 4	ps-1	$⊢ (K \in HL \land (Q \in A \land R \in A \land Q \neq R) \land (P \in A \land R \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R) \leftrightarrow Q \underset{˙}{\lor} R = P \underset{˙}{\lor} R)$
54	36 39 38 52 37 38 53	syl132anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R) \leftrightarrow Q \underset{˙}{\lor} R = P \underset{˙}{\lor} R)$
55	54	biimpd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to Q \underset{˙}{\lor} R = P \underset{˙}{\lor} R)$
56		eqcom	$⊢ Q \underset{˙}{\lor} R = P \underset{˙}{\lor} R \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
57	55 56	imbitrdi	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
58	51 57	syld	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
59	58	necon3ad	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to (P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
60	40 59	mpd	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
61	1 2 3 4	2llnma1	$⊢ (K \in HL \land (P \in A \land R \in A \land Q \in A) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) = R$
62	36 37 38 39 60 61	syl131anc	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \land Q \neq R) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) = R$
63	35 62	pm2.61dane	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to (R \underset{˙}{\lor} P) \underset{˙}{\land} (R \underset{˙}{\lor} Q) = R$
64	13 63	eqtrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land P \underset{˙}{\lor} R \neq Q \underset{˙}{\lor} R) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (Q \underset{˙}{\lor} R) = R$

Metamath Proof Explorer

Theorem 2llnma3r

Proof