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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cvlsupr2.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlsupr2.j ⊢ ∨ = ( join ‘ 𝐾 )
Assertion cvlsupr2 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ( ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )

Proof

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