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

Metamath Proof Explorer

Theorem cdleme22a

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, 30-Nov-2012)

Ref Expression
Hypotheses cdleme22.l ⊢ ≤ = ( le ‘ 𝐾 )
cdleme22.j ⊢ ∨ = ( join ‘ 𝐾 )
cdleme22.m ⊢ ∧ = ( meet ‘ 𝐾 )
cdleme22.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
cdleme22.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
cdleme22.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion cdleme22a ( ( ( 𝐾 ∈ 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 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
9 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
10 simp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≠ 𝑄 )
11 simp31l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ∈ 𝐴 )
12 simp31r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ 𝑊 )
13 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
14 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑇 ∈ 𝐴 )
15 1 2 4 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → 𝑉 ≤ ( 𝑇 ∨ 𝑉 ) )
16 13 14 11 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ ( 𝑇 ∨ 𝑉 ) )
17 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) )
18 16 17 breqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) )
19 1 2 3 4 5 6 cdleme22aa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 = 𝑈 )
20 7 8 9 10 11 12 18 19 syl133anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑇 ∨ 𝑉 ) = ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 = 𝑈 )