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

Metamath Proof Explorer

Theorem cdleme22aa

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph, 3rd line on p. 115. Show that t \/ v = p \/ q implies v = u. (Contributed by NM, 2-Dec-2012)

Ref Expression
Hypotheses cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme22.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion cdleme22aa ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 = 𝑈 )

Proof

Step Hyp Ref Expression
1 cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme22.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
7 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) )
8 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ 𝑊 )
9 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
10 9 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ Lat )
11 simp31 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ∈ 𝐴 )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 4 atbase ⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
14 11 13 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ∈ ( Base ‘ 𝐾 ) )
15 simp21l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
16 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
17 12 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
18 9 15 16 17 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
19 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ 𝐻 )
20 12 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21 19 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
22 12 1 3 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑉 ≤ 𝑊 ) ↔ 𝑉 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
23 10 14 18 21 22 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑉 ≤ 𝑊 ) ↔ 𝑉 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ) )
24 7 8 23 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) )
25 24 6 breqtrrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ 𝑈 )
26 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
27 9 26 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ AtLat )
28 simp21r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑃 ≤ 𝑊 )
29 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≠ 𝑄 )
30 1 2 3 4 5 6 cdleme0a ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑈 ∈ 𝐴 )
31 9 19 15 28 16 29 30 syl222anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑈 ∈ 𝐴 )
32 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑉 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑉 ≤ 𝑈 ↔ 𝑉 = 𝑈 ) )
33 27 11 31 32 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑉 ≤ 𝑈 ↔ 𝑉 = 𝑈 ) )
34 25 33 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 = 𝑈 )