Metamath Proof Explorer

Theorem 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 
|- .<_ = ( le ` K )
cvlsupr2.j 
|- .\/ = ( join ` K )
Assertion cvlsupr2 
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= Q ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) )

Proof

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