Metamath Proof Explorer


Theorem cvrat3

Description: A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat3.b B=BaseK
cvrat3.l ˙=K
cvrat3.j ˙=joinK
cvrat3.m ˙=meetK
cvrat3.a A=AtomsK
Assertion cvrat3 KHLXBPAQAPQ¬Q˙XP˙X˙QX˙P˙QA

Proof

Step Hyp Ref Expression
1 cvrat3.b B=BaseK
2 cvrat3.l ˙=K
3 cvrat3.j ˙=joinK
4 cvrat3.m ˙=meetK
5 cvrat3.a A=AtomsK
6 eqid K=K
7 1 2 3 6 5 cvr1 KHLXBQA¬Q˙XXKX˙Q
8 7 3adant3r2 KHLXBPAQA¬Q˙XXKX˙Q
9 8 biimpa KHLXBPAQA¬Q˙XXKX˙Q
10 9 adantrr KHLXBPAQA¬Q˙XP˙X˙QXKX˙Q
11 hllat KHLKLat
12 11 adantr KHLXBPAQAKLat
13 simpr2 KHLXBPAQAPA
14 1 5 atbase PAPB
15 13 14 syl KHLXBPAQAPB
16 simpr3 KHLXBPAQAQA
17 1 5 atbase QAQB
18 16 17 syl KHLXBPAQAQB
19 1 3 latjcom KLatPBQBP˙Q=Q˙P
20 12 15 18 19 syl3anc KHLXBPAQAP˙Q=Q˙P
21 20 oveq2d KHLXBPAQAX˙P˙Q=X˙Q˙P
22 simpr1 KHLXBPAQAXB
23 1 3 latjass KLatXBQBPBX˙Q˙P=X˙Q˙P
24 12 22 18 15 23 syl13anc KHLXBPAQAX˙Q˙P=X˙Q˙P
25 21 24 eqtr4d KHLXBPAQAX˙P˙Q=X˙Q˙P
26 25 adantr KHLXBPAQAP˙X˙QX˙P˙Q=X˙Q˙P
27 1 3 latjcl KLatXBQBX˙QB
28 12 22 18 27 syl3anc KHLXBPAQAX˙QB
29 1 2 3 latjlej2 KLatPBX˙QBX˙QBP˙X˙QX˙Q˙P˙X˙Q˙X˙Q
30 12 15 28 28 29 syl13anc KHLXBPAQAP˙X˙QX˙Q˙P˙X˙Q˙X˙Q
31 30 imp KHLXBPAQAP˙X˙QX˙Q˙P˙X˙Q˙X˙Q
32 26 31 eqbrtrd KHLXBPAQAP˙X˙QX˙P˙Q˙X˙Q˙X˙Q
33 1 3 latjidm KLatX˙QBX˙Q˙X˙Q=X˙Q
34 12 28 33 syl2anc KHLXBPAQAX˙Q˙X˙Q=X˙Q
35 34 adantr KHLXBPAQAP˙X˙QX˙Q˙X˙Q=X˙Q
36 32 35 breqtrd KHLXBPAQAP˙X˙QX˙P˙Q˙X˙Q
37 simpl KHLXBPAQAKHL
38 2 3 5 hlatlej2 KHLPAQAQ˙P˙Q
39 37 13 16 38 syl3anc KHLXBPAQAQ˙P˙Q
40 1 3 latjcl KLatPBQBP˙QB
41 12 15 18 40 syl3anc KHLXBPAQAP˙QB
42 1 2 3 latjlej2 KLatQBP˙QBXBQ˙P˙QX˙Q˙X˙P˙Q
43 12 18 41 22 42 syl13anc KHLXBPAQAQ˙P˙QX˙Q˙X˙P˙Q
44 39 43 mpd KHLXBPAQAX˙Q˙X˙P˙Q
45 44 adantr KHLXBPAQAP˙X˙QX˙Q˙X˙P˙Q
46 1 3 latjcl KLatXBP˙QBX˙P˙QB
47 12 22 41 46 syl3anc KHLXBPAQAX˙P˙QB
48 1 2 latasymb KLatX˙P˙QBX˙QBX˙P˙Q˙X˙QX˙Q˙X˙P˙QX˙P˙Q=X˙Q
49 12 47 28 48 syl3anc KHLXBPAQAX˙P˙Q˙X˙QX˙Q˙X˙P˙QX˙P˙Q=X˙Q
50 49 adantr KHLXBPAQAP˙X˙QX˙P˙Q˙X˙QX˙Q˙X˙P˙QX˙P˙Q=X˙Q
51 36 45 50 mpbi2and KHLXBPAQAP˙X˙QX˙P˙Q=X˙Q
52 51 breq2d KHLXBPAQAP˙X˙QXKX˙P˙QXKX˙Q
53 52 adantrl KHLXBPAQA¬Q˙XP˙X˙QXKX˙P˙QXKX˙Q
54 10 53 mpbird KHLXBPAQA¬Q˙XP˙X˙QXKX˙P˙Q
55 54 ex KHLXBPAQA¬Q˙XP˙X˙QXKX˙P˙Q
56 1 3 4 6 cvrexch KHLXBP˙QBX˙P˙QKP˙QXKX˙P˙Q
57 37 22 41 56 syl3anc KHLXBPAQAX˙P˙QKP˙QXKX˙P˙Q
58 55 57 sylibrd KHLXBPAQA¬Q˙XP˙X˙QX˙P˙QKP˙Q
59 58 adantr KHLXBPAQAPQ¬Q˙XP˙X˙QX˙P˙QKP˙Q
60 1 4 latmcl KLatXBP˙QBX˙P˙QB
61 12 22 41 60 syl3anc KHLXBPAQAX˙P˙QB
62 1 3 6 5 cvrat2 KHLX˙P˙QBPAQAPQX˙P˙QKP˙QX˙P˙QA
63 62 3expia KHLX˙P˙QBPAQAPQX˙P˙QKP˙QX˙P˙QA
64 37 61 13 16 63 syl13anc KHLXBPAQAPQX˙P˙QKP˙QX˙P˙QA
65 64 expdimp KHLXBPAQAPQX˙P˙QKP˙QX˙P˙QA
66 59 65 syld KHLXBPAQAPQ¬Q˙XP˙X˙QX˙P˙QA
67 66 exp4b KHLXBPAQAPQ¬Q˙XP˙X˙QX˙P˙QA
68 67 3impd KHLXBPAQAPQ¬Q˙XP˙X˙QX˙P˙QA