cdleme8

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. C represents s_1. In their notation, we prove p \/ s_1 = p \/ s. (Contributed by NM, 9-Jun-2012)

	Ref	Expression
Hypotheses	cdleme8.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme8.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme8.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme8.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme8.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme8.4	⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
Assertion	cdleme8	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝐶 ) = ( 𝑃 ∨ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		cdleme8.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme8.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme8.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme8.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme8.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme8.4	⊢ 𝐶 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
7	6	oveq2i	⊢ ( 𝑃 ∨ 𝐶 ) = ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) )
8		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝐾 ∈ HL )
9		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
10	8	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝐾 ∈ Lat )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13	9 12	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
14	11 4	atbase	⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
15	14	3ad2ant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
16	11 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
17	10 13 15 16	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
18		simp1r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑊 ∈ 𝐻 )
19	11 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
20	18 19	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
21	11 1 2	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
22	10 13 15 21	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) )
23	11 1 2 3 4	atmod3i1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
24	8 9 17 20 22 23	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) )
25		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
26	1 2 25 4 5	lhpjat2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
27	26	3adant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
28	27	oveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 𝑃 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) )
29		hlol	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
30	8 29	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → 𝐾 ∈ OL )
31	11 3 25	olm11	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑆 ) )
32	30 17 31	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑆 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑃 ∨ 𝑆 ) )
33	24 28 32	3eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( 𝑃 ∨ 𝑆 ) )
34	7 33	syl5eq	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝐶 ) = ( 𝑃 ∨ 𝑆 ) )

Metamath Proof Explorer

Theorem cdleme8

Proof