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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ∧ 𝑉 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑉 = 𝑈 )