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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
1cvrjat.l ⊢ ≤ = ( le ‘ 𝐾 )
1cvrjat.j ⊢ ∨ = ( join ‘ 𝐾 )
1cvrjat.u ⊢ 1 = ( 1. ‘ 𝐾 )
1cvrjat.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
1cvrjat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 1cvrjat ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∨ 𝑃 ) = 1 )

Proof

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