Metamath Proof Explorer


Theorem cdleme41sn3aw

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(r) is different on and off the P .\/ Q line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013)

Ref Expression
Hypotheses cdleme41.b 𝐵 = ( Base ‘ 𝐾 )
cdleme41.l = ( le ‘ 𝐾 )
cdleme41.j = ( join ‘ 𝐾 )
cdleme41.m = ( meet ‘ 𝐾 )
cdleme41.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme41.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme41.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme41.d 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
cdleme41.e 𝐸 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
cdleme41.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
cdleme41.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) )
cdleme41.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
Assertion cdleme41sn3aw ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → 𝑅 / 𝑠 𝑁 𝑆 / 𝑠 𝑁 )

Proof

Step Hyp Ref Expression
1 cdleme41.b 𝐵 = ( Base ‘ 𝐾 )
2 cdleme41.l = ( le ‘ 𝐾 )
3 cdleme41.j = ( join ‘ 𝐾 )
4 cdleme41.m = ( meet ‘ 𝐾 )
5 cdleme41.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme41.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme41.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 cdleme41.d 𝐷 = ( ( 𝑠 𝑈 ) ( 𝑄 ( ( 𝑃 𝑠 ) 𝑊 ) ) )
9 cdleme41.e 𝐸 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
10 cdleme41.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
11 cdleme41.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) )
12 cdleme41.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
13 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
14 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → 𝑃𝑄 )
15 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) )
16 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → 𝑅 ( 𝑃 𝑄 ) )
17 eqid ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑅 𝑡 ) 𝑊 ) ) ) = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑅 𝑡 ) 𝑊 ) ) )
18 eqid ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑅 𝑡 ) 𝑊 ) ) ) ) ) = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑅 𝑡 ) 𝑊 ) ) ) ) )
19 1 2 3 4 5 6 7 8 9 10 11 12 17 18 cdleme41sn3a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 ( 𝑃 𝑄 ) )
20 13 14 15 16 19 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → 𝑅 / 𝑠 𝑁 ( 𝑃 𝑄 ) )
21 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) )
22 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
23 1 2 3 4 5 6 7 8 12 cdleme35sn3a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) → ¬ 𝑆 / 𝑠 𝑁 ( 𝑃 𝑄 ) )
24 13 14 21 22 23 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → ¬ 𝑆 / 𝑠 𝑁 ( 𝑃 𝑄 ) )
25 nbrne2 ( ( 𝑅 / 𝑠 𝑁 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 / 𝑠 𝑁 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 𝑆 / 𝑠 𝑁 )
26 20 24 25 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ) → 𝑅 / 𝑠 𝑁 𝑆 / 𝑠 𝑁 )