Metamath Proof Explorer


Theorem cdleme25a

Description: Lemma for cdleme25b . (Contributed by NM, 1-Jan-2013)

Ref Expression
Hypotheses cdleme24.b 𝐵 = ( Base ‘ 𝐾 )
cdleme24.l = ( le ‘ 𝐾 )
cdleme24.j = ( join ‘ 𝐾 )
cdleme24.m = ( meet ‘ 𝐾 )
cdleme24.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme24.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme24.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme24.f 𝐹 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
cdleme24.n 𝑁 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑠 ) 𝑊 ) ) )
Assertion cdleme25a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → ∃ 𝑠𝐴 ( ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) ∧ 𝑁𝐵 ) )

Proof

Step Hyp Ref Expression
1 cdleme24.b 𝐵 = ( Base ‘ 𝐾 )
2 cdleme24.l = ( le ‘ 𝐾 )
3 cdleme24.j = ( join ‘ 𝐾 )
4 cdleme24.m = ( meet ‘ 𝐾 )
5 cdleme24.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme24.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme24.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 cdleme24.f 𝐹 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
9 cdleme24.n 𝑁 = ( ( 𝑃 𝑄 ) ( 𝐹 ( ( 𝑅 𝑠 ) 𝑊 ) ) )
10 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
11 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
12 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
13 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
14 simp3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃𝑄 )
15 2 3 5 6 cdlemb2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → ∃ 𝑠𝐴 ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) )
16 10 11 12 13 14 15 syl221anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → ∃ 𝑠𝐴 ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) )
17 10 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → 𝐾 ∈ HL )
18 11 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → 𝑊𝐻 )
19 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
20 19 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → 𝑃𝐴 )
21 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
22 21 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → 𝑄𝐴 )
23 simpl2l ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → 𝑅𝐴 )
24 simpr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → 𝑠𝐴 )
25 2 3 4 5 6 7 8 9 1 cdleme22gb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑠𝐴 ) ) → 𝑁𝐵 )
26 17 18 20 22 23 24 25 syl222anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → 𝑁𝐵 )
27 26 a1d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → ( ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) → 𝑁𝐵 ) )
28 27 ancld ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) ∧ 𝑠𝐴 ) → ( ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) → ( ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) ∧ 𝑁𝐵 ) ) )
29 28 reximdva ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → ( ∃ 𝑠𝐴 ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) → ∃ 𝑠𝐴 ( ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) ∧ 𝑁𝐵 ) ) )
30 16 29 mpd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → ∃ 𝑠𝐴 ( ( ¬ 𝑠 𝑊 ∧ ¬ 𝑠 ( 𝑃 𝑄 ) ) ∧ 𝑁𝐵 ) )