cdleme10

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

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

Proof

Step	Hyp	Ref	Expression
1		cdleme10.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdleme10.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdleme10.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdleme10.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdleme10.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdleme10.d	⊢ 𝐷 = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
7	6	oveq2i	⊢ ( 𝑆 ∨ 𝐷 ) = ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) )
8		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
9		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ∈ 𝐴 )
10		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ∈ 𝐴 )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
13	8 10 9 12	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
14		simp1r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
15	11 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16	14 15	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
17	8	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
18	11 4	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
19	18	3ad2ant2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
20	11 4	atbase	⊢ ( 𝑆 ∈ 𝐴 → 𝑆 ∈ ( Base ‘ 𝐾 ) )
21	9 20	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
22	11 1 2	latlej2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) )
23	17 19 21 22	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) )
24	11 1 2 3 4	atmod3i1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) )
25	8 9 13 16 23 24	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) )
26	11 2	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ∨ 𝑆 ) = ( 𝑆 ∨ 𝑅 ) )
27	17 19 21 26	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑅 ∨ 𝑆 ) = ( 𝑆 ∨ 𝑅 ) )
28		eqid	⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
29	1 2 28 4 5	lhpjat2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
30	29	3adant2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝑊 ) = ( 1. ‘ 𝐾 ) )
31	27 30	oveq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑅 ∨ 𝑆 ) ∧ ( 𝑆 ∨ 𝑊 ) ) = ( ( 𝑆 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) )
32		hlol	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
33	8 32	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
34	11 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
35	17 21 19 34	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
36	11 3 28	olm11	⊢ ( ( 𝐾 ∈ OL ∧ ( 𝑆 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑆 ∨ 𝑅 ) )
37	33 35 36	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( ( 𝑆 ∨ 𝑅 ) ∧ ( 1. ‘ 𝐾 ) ) = ( 𝑆 ∨ 𝑅 ) )
38	25 31 37	3eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) = ( 𝑆 ∨ 𝑅 ) )
39	7 38	eqtrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ∧ ( 𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊 ) ) → ( 𝑆 ∨ 𝐷 ) = ( 𝑆 ∨ 𝑅 ) )

Metamath Proof Explorer

Theorem cdleme10

Proof