Metamath Proof Explorer


Theorem cdleme22gb

Description: Utility lemma for Lemma E in Crawley p. 115. (Contributed by NM, 5-Dec-2012)

Ref Expression
Hypotheses cdleme18d.l = ( le ‘ 𝐾 )
cdleme18d.j = ( join ‘ 𝐾 )
cdleme18d.m = ( meet ‘ 𝐾 )
cdleme18d.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme18d.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme18d.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme18d.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
cdleme18d.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) )
cdleme22.b 𝐵 = ( Base ‘ 𝐾 )
Assertion cdleme22gb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝐺𝐵 )

Proof

Step Hyp Ref Expression
1 cdleme18d.l = ( le ‘ 𝐾 )
2 cdleme18d.j = ( join ‘ 𝐾 )
3 cdleme18d.m = ( meet ‘ 𝐾 )
4 cdleme18d.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme18d.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme18d.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme18d.f 𝐹 = ( ( 𝑆 𝑈 ) ( 𝑄 ( ( 𝑃 𝑆 ) 𝑊 ) ) )
8 cdleme18d.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) )
9 cdleme22.b 𝐵 = ( Base ‘ 𝐾 )
10 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝐾 ∈ HL )
11 10 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝐾 ∈ Lat )
12 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑃𝐴 )
13 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑄𝐴 )
14 9 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ 𝐵 )
15 10 12 13 14 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( 𝑃 𝑄 ) ∈ 𝐵 )
16 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
17 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑆𝐴 )
18 1 2 3 4 5 6 7 9 cdleme1b ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴𝑆𝐴 ) ) → 𝐹𝐵 )
19 16 12 13 17 18 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝐹𝐵 )
20 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑅𝐴 )
21 9 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴 ) → ( 𝑅 𝑆 ) ∈ 𝐵 )
22 10 20 17 21 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( 𝑅 𝑆 ) ∈ 𝐵 )
23 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑊𝐻 )
24 9 5 lhpbase ( 𝑊𝐻𝑊𝐵 )
25 23 24 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝑊𝐵 )
26 9 3 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑅 𝑆 ) ∈ 𝐵𝑊𝐵 ) → ( ( 𝑅 𝑆 ) 𝑊 ) ∈ 𝐵 )
27 11 22 25 26 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑅 𝑆 ) 𝑊 ) ∈ 𝐵 )
28 9 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝐹𝐵 ∧ ( ( 𝑅 𝑆 ) 𝑊 ) ∈ 𝐵 ) → ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) ∈ 𝐵 )
29 11 19 27 28 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) ∈ 𝐵 )
30 9 3 latmcl ( ( 𝐾 ∈ Lat ∧ ( 𝑃 𝑄 ) ∈ 𝐵 ∧ ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) ∈ 𝐵 ) → ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) ) ∈ 𝐵 )
31 11 15 29 30 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑆 ) 𝑊 ) ) ) ∈ 𝐵 )
32 8 31 eqeltrid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ) → 𝐺𝐵 )