cvlsupr2

Description: Two equivalent ways of expressing that R is a superposition of P and Q . (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	cvlsupr2.a	$⊢ A = Atoms (K)$
	cvlsupr2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvlsupr2.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	cvlsupr2	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$

Proof

Step	Hyp	Ref	Expression
1		cvlsupr2.a	$⊢ A = Atoms (K)$
2		cvlsupr2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvlsupr2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		simpl3	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to P \neq Q$
5	4	necomd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to Q \neq P$
6		simplr	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = P) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
7		oveq2	$⊢ R = P \to P \underset{˙}{\lor} R = P \underset{˙}{\lor} P$
8		oveq2	$⊢ R = P \to Q \underset{˙}{\lor} R = Q \underset{˙}{\lor} P$
9	7 8	eqeq12d	$⊢ R = P \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow P \underset{˙}{\lor} P = Q \underset{˙}{\lor} P)$
10		eqcom	$⊢ P \underset{˙}{\lor} P = Q \underset{˙}{\lor} P \leftrightarrow Q \underset{˙}{\lor} P = P \underset{˙}{\lor} P$
11	9 10	bitrdi	$⊢ R = P \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow Q \underset{˙}{\lor} P = P \underset{˙}{\lor} P)$
12	11	adantl	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = P) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow Q \underset{˙}{\lor} P = P \underset{˙}{\lor} P)$
13	6 12	mpbid	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = P) \to Q \underset{˙}{\lor} P = P \underset{˙}{\lor} P$
14		simpl1	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to K \in CvLat$
15		cvllat	$⊢ K \in CvLat \to K \in Lat$
16	14 15	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to K \in Lat$
17		simpl21	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to P \in A$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19	18 1	atbase	$⊢ P \in A \to P \in {Base}_{K}$
20	17 19	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to P \in {Base}_{K}$
21	18 3	latjidm	$⊢ (K \in Lat \land P \in {Base}_{K}) \to P \underset{˙}{\lor} P = P$
22	16 20 21	syl2anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to P \underset{˙}{\lor} P = P$
23	22	adantr	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = P) \to P \underset{˙}{\lor} P = P$
24	13 23	eqtrd	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = P) \to Q \underset{˙}{\lor} P = P$
25	24	ex	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (R = P \to Q \underset{˙}{\lor} P = P)$
26		simpl22	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to Q \in A$
27	18 1	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
28	26 27	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to Q \in {Base}_{K}$
29	18 2 3	latleeqj1	$⊢ (K \in Lat \land Q \in {Base}_{K} \land P \in {Base}_{K}) \to (Q \underset{˙}{\leq} P \leftrightarrow Q \underset{˙}{\lor} P = P)$
30	16 28 20 29	syl3anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (Q \underset{˙}{\leq} P \leftrightarrow Q \underset{˙}{\lor} P = P)$
31		cvlatl	$⊢ K \in CvLat \to K \in AtLat$
32	14 31	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to K \in AtLat$
33	2 1	atcmp	$⊢ (K \in AtLat \land Q \in A \land P \in A) \to (Q \underset{˙}{\leq} P \leftrightarrow Q = P)$
34	32 26 17 33	syl3anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (Q \underset{˙}{\leq} P \leftrightarrow Q = P)$
35	30 34	bitr3d	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (Q \underset{˙}{\lor} P = P \leftrightarrow Q = P)$
36	25 35	sylibd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (R = P \to Q = P)$
37	36	necon3d	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (Q \neq P \to R \neq P)$
38	5 37	mpd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to R \neq P$
39		simplr	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = Q) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
40		oveq2	$⊢ R = Q \to P \underset{˙}{\lor} R = P \underset{˙}{\lor} Q$
41		oveq2	$⊢ R = Q \to Q \underset{˙}{\lor} R = Q \underset{˙}{\lor} Q$
42	40 41	eqeq12d	$⊢ R = Q \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q)$
43	42	adantl	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = Q) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q)$
44	39 43	mpbid	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = Q) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} Q$
45	18 3	latjidm	$⊢ (K \in Lat \land Q \in {Base}_{K}) \to Q \underset{˙}{\lor} Q = Q$
46	16 28 45	syl2anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to Q \underset{˙}{\lor} Q = Q$
47	46	adantr	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = Q) \to Q \underset{˙}{\lor} Q = Q$
48	44 47	eqtrd	$⊢ (((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \land R = Q) \to P \underset{˙}{\lor} Q = Q$
49	48	ex	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (R = Q \to P \underset{˙}{\lor} Q = Q)$
50	18 2 3	latleeqj1	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to (P \underset{˙}{\leq} Q \leftrightarrow P \underset{˙}{\lor} Q = Q)$
51	16 20 28 50	syl3anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (P \underset{˙}{\leq} Q \leftrightarrow P \underset{˙}{\lor} Q = Q)$
52	2 1	atcmp	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \underset{˙}{\leq} Q \leftrightarrow P = Q)$
53	32 17 26 52	syl3anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (P \underset{˙}{\leq} Q \leftrightarrow P = Q)$
54	51 53	bitr3d	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (P \underset{˙}{\lor} Q = Q \leftrightarrow P = Q)$
55	49 54	sylibd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (R = Q \to P = Q)$
56	55	necon3d	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (P \neq Q \to R \neq Q)$
57	4 56	mpd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to R \neq Q$
58		simpl23	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to R \in A$
59	18 1	atbase	$⊢ R \in A \to R \in {Base}_{K}$
60	58 59	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to R \in {Base}_{K}$
61	18 2 3	latlej1	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
62	16 28 60 61	syl3anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
63		simpr	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
64	62 63	breqtrrd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
65	2 3 1	cvlatexch1	$⊢ (K \in CvLat \land (Q \in A \land R \in A \land P \in A) \land Q \neq P) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
66	14 26 58 17 5 65	syl131anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
67	64 66	mpd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
68	38 57 67	3jca	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
69		simpr3	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
70		simpl1	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in CvLat$
71	70 15	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
72		simpl21	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
73	72 19	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in {Base}_{K}$
74		simpl22	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
75	74 27	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in {Base}_{K}$
76	18 3	latjcom	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
77	71 73 75 76	syl3anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
78	77	breq2d	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow R \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
79		simpl23	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in A$
80		simpr2	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \neq Q$
81	2 3 1	cvlatexch1	$⊢ (K \in CvLat \land (R \in A \land P \in A \land Q \in A) \land R \neq Q) \to (R \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
82	70 79 72 74 80 81	syl131anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
83		simpr1	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \neq P$
84	83	necomd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq R$
85	2 3 1	cvlatexchb2	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
86	70 72 74 79 84 85	syl131anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
87	82 86	sylibd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} (Q \underset{˙}{\lor} P) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
88	78 87	sylbid	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
89	69 88	mpd	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \land (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
90	68 89	impbida	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow (R \neq P \land R \neq Q \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$

Metamath Proof Explorer

Theorem cvlsupr2

Proof