This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1cvrat

Description: Create an atom under an element covered by the lattice unity. Part of proof of Lemma B in Crawley p. 112. (Contributed by NM, 30-Apr-2012)

Ref Expression
Hypotheses 1cvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
1cvrat.l ⊢ ≤ = ( le ‘ 𝐾 )
1cvrat.j ⊢ ∨ = ( join ‘ 𝐾 )
1cvrat.m ⊢ ∧ = ( meet ‘ 𝐾 )
1cvrat.u ⊢ 1 = ( 1. ‘ 𝐾 )
1cvrat.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
1cvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 1cvrat ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 1cvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 1cvrat.l ⊢ ≤ = ( le ‘ 𝐾 )
3 1cvrat.j ⊢ ∨ = ( join ‘ 𝐾 )
4 1cvrat.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 1cvrat.u ⊢ 1 = ( 1. ‘ 𝐾 )
6 1cvrat.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
7 1cvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
9 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
10 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐴 )
11 1 7 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
12 10 11 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑃 ∈ 𝐵 )
13 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐴 )
14 1 7 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
15 13 14 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ∈ 𝐵 )
16 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
17 9 12 15 16 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
18 17 oveq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑋 ) )
19 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑄 ∨ 𝑃 ) ∈ 𝐵 )
20 9 15 12 19 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑄 ∨ 𝑃 ) ∈ 𝐵 )
21 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
22 1 4 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ 𝑃 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) )
23 9 20 21 22 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑄 ∨ 𝑃 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) )
24 18 23 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) = ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) )
25 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ HL )
26 21 13 10 3jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) )
27 simp31 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑃 ≠ 𝑄 )
28 27 necomd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ≠ 𝑃 )
29 simp33 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ¬ 𝑃 ≤ 𝑋 )
30 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
31 30 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝐾 ∈ OP )
32 1 2 5 ople1 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑄 ∈ 𝐵 ) → 𝑄 ≤ 1 )
33 31 15 32 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ≤ 1 )
34 simp32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑋 𝐶 1 )
35 1 2 3 5 6 7 1cvrjat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∨ 𝑃 ) = 1 )
36 25 21 10 34 29 35 syl32anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∨ 𝑃 ) = 1 )
37 33 36 breqtrrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) )
38 1 2 3 4 7 cvrat3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ) → ( ( 𝑄 ≠ 𝑃 ∧ ¬ 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) → ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) ∈ 𝐴 ) )
39 38 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ) ∧ ( 𝑄 ≠ 𝑃 ∧ ¬ 𝑃 ≤ 𝑋 ∧ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ) → ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) ∈ 𝐴 )
40 25 26 28 29 37 39 syl23anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( 𝑋 ∧ ( 𝑄 ∨ 𝑃 ) ) ∈ 𝐴 )
41 24 40 eqeltrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑋 ) ∈ 𝐴 )