Metamath Proof Explorer

Theorem 1cvrjat

Description: An element covered by the lattice unity, when joined with an atom not under it, equals the lattice unity. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses 1cvrjat.b ⊢B=BaseK
1cvrjat.l ⊢≤˙=≤K
1cvrjat.j ⊢∨˙=join⁡K
1cvrjat.u ⊢1˙=1.⁡K
1cvrjat.c ⊢C=⋖K
1cvrjat.a ⊢A=Atoms⁡K
Assertion 1cvrjat ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→X∨˙P=1˙

Proof

Step Hyp Ref Expression
1 1cvrjat.b ⊢B=BaseK
2 1cvrjat.l ⊢≤˙=≤K
3 1cvrjat.j ⊢∨˙=join⁡K
4 1cvrjat.u ⊢1˙=1.⁡K
5 1cvrjat.c ⊢C=⋖K
6 1cvrjat.a ⊢A=Atoms⁡K
7 simprr ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→¬P≤˙X
8 1 2 3 5 6 cvr1 ⊢K∈HL∧X∈B∧P∈A→¬P≤˙X↔XCX∨˙P
9 8 adantr ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→¬P≤˙X↔XCX∨˙P
10 7 9 mpbid ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→XCX∨˙P
11 simpl1 ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→K∈HL
12 hlop ⊢K∈HL→K∈OP
13 11 12 syl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→K∈OP
14 simpl2 ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→X∈B
15 11 hllatd ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→K∈Lat
16 simpl3 ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→P∈A
17 1 6 atbase ⊢P∈A→P∈B
18 16 17 syl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→P∈B
19 1 3 latjcl ⊢K∈Lat∧X∈B∧P∈B→X∨˙P∈B
20 15 14 18 19 syl3anc ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→X∨˙P∈B
21 eqid ⊢oc⁡K=oc⁡K
22 1 21 5 cvrcon3b ⊢K∈OP∧X∈B∧X∨˙P∈B→XCX∨˙P↔oc⁡K⁡X∨˙PCoc⁡K⁡X
23 13 14 20 22 syl3anc ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→XCX∨˙P↔oc⁡K⁡X∨˙PCoc⁡K⁡X
24 10 23 mpbid ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡X∨˙PCoc⁡K⁡X
25 hlatl ⊢K∈HL→K∈AtLat
26 11 25 syl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→K∈AtLat
27 1 21 opoccl ⊢K∈OP∧X∨˙P∈B→oc⁡K⁡X∨˙P∈B
28 13 20 27 syl2anc ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡X∨˙P∈B
29 1 21 opoccl ⊢K∈OP∧X∈B→oc⁡K⁡X∈B
30 13 14 29 syl2anc ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡X∈B
31 eqid ⊢0.⁡K=0.⁡K
32 31 4 21 opoc1 ⊢K∈OP→oc⁡K⁡1˙=0.⁡K
33 11 12 32 3syl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡1˙=0.⁡K
34 simprl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→XC1˙
35 1 4 op1cl ⊢K∈OP→1˙∈B
36 11 12 35 3syl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→1˙∈B
37 1 21 5 cvrcon3b ⊢K∈OP∧X∈B∧1˙∈B→XC1˙↔oc⁡K⁡1˙Coc⁡K⁡X
38 13 14 36 37 syl3anc ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→XC1˙↔oc⁡K⁡1˙Coc⁡K⁡X
39 34 38 mpbid ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡1˙Coc⁡K⁡X
40 33 39 eqbrtrrd ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→0.⁡KCoc⁡K⁡X
41 1 31 5 6 isat ⊢K∈HL→oc⁡K⁡X∈A↔oc⁡K⁡X∈B∧0.⁡KCoc⁡K⁡X
42 11 41 syl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡X∈A↔oc⁡K⁡X∈B∧0.⁡KCoc⁡K⁡X
43 30 40 42 mpbir2and ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡X∈A
44 1 2 31 5 6 atcvreq0 ⊢K∈AtLat∧oc⁡K⁡X∨˙P∈B∧oc⁡K⁡X∈A→oc⁡K⁡X∨˙PCoc⁡K⁡X↔oc⁡K⁡X∨˙P=0.⁡K
45 26 28 43 44 syl3anc ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡X∨˙PCoc⁡K⁡X↔oc⁡K⁡X∨˙P=0.⁡K
46 24 45 mpbid ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡X∨˙P=0.⁡K
47 46 fveq2d ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡oc⁡K⁡X∨˙P=oc⁡K⁡0.⁡K
48 1 21 opococ ⊢K∈OP∧X∨˙P∈B→oc⁡K⁡oc⁡K⁡X∨˙P=X∨˙P
49 13 20 48 syl2anc ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡oc⁡K⁡X∨˙P=X∨˙P
50 31 4 21 opoc0 ⊢K∈OP→oc⁡K⁡0.⁡K=1˙
51 11 12 50 3syl ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→oc⁡K⁡0.⁡K=1˙
52 47 49 51 3eqtr3d ⊢K∈HL∧X∈B∧P∈A∧XC1˙∧¬P≤˙X→X∨˙P=1˙