Metamath Proof Explorer


Theorem cdleme40m

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT Use proof idea from cdleme32sn1awN . (Contributed by NM, 18-Mar-2013)

Ref Expression
Hypotheses cdleme40.b 𝐵 = ( Base ‘ 𝐾 )
cdleme40.l = ( le ‘ 𝐾 )
cdleme40.j = ( join ‘ 𝐾 )
cdleme40.m = ( meet ‘ 𝐾 )
cdleme40.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme40.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme40.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme40.e 𝐸 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
cdleme40.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
cdleme40.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) )
cdleme40.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
cdleme40a1.y 𝑌 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑅 𝑡 ) 𝑊 ) ) )
cdleme40a1.c 𝐶 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) )
cdleme40.t 𝑇 = ( ( 𝑣 𝑈 ) ( 𝑄 ( ( 𝑃 𝑣 ) 𝑊 ) ) )
cdleme40.f 𝐹 = ( ( 𝑃 𝑄 ) ( 𝑇 ( ( 𝑆 𝑣 ) 𝑊 ) ) )
Assertion cdleme40m ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑅 / 𝑠 𝑁𝐹 )

Proof

Step Hyp Ref Expression
1 cdleme40.b 𝐵 = ( Base ‘ 𝐾 )
2 cdleme40.l = ( le ‘ 𝐾 )
3 cdleme40.j = ( join ‘ 𝐾 )
4 cdleme40.m = ( meet ‘ 𝐾 )
5 cdleme40.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdleme40.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdleme40.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
8 cdleme40.e 𝐸 = ( ( 𝑡 𝑈 ) ( 𝑄 ( ( 𝑃 𝑡 ) 𝑊 ) ) )
9 cdleme40.g 𝐺 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑠 𝑡 ) 𝑊 ) ) )
10 cdleme40.i 𝐼 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝐺 ) )
11 cdleme40.n 𝑁 = if ( 𝑠 ( 𝑃 𝑄 ) , 𝐼 , 𝐷 )
12 cdleme40a1.y 𝑌 = ( ( 𝑃 𝑄 ) ( 𝐸 ( ( 𝑅 𝑡 ) 𝑊 ) ) )
13 cdleme40a1.c 𝐶 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) )
14 cdleme40.t 𝑇 = ( ( 𝑣 𝑈 ) ( 𝑄 ( ( 𝑃 𝑣 ) 𝑊 ) ) )
15 cdleme40.f 𝐹 = ( ( 𝑃 𝑄 ) ( 𝑇 ( ( 𝑆 𝑣 ) 𝑊 ) ) )
16 simp22l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑅𝐴 )
17 simp3l1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑅 ( 𝑃 𝑄 ) )
18 9 10 11 12 13 cdleme31sn1c ( ( 𝑅𝐴𝑅 ( 𝑃 𝑄 ) ) → 𝑅 / 𝑠 𝑁 = 𝐶 )
19 16 17 18 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑅 / 𝑠 𝑁 = 𝐶 )
20 1 fvexi 𝐵 ∈ V
21 nfv 𝑡 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) )
22 nfra1 𝑡𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 )
23 nfcv 𝑡 𝐵
24 22 23 nfriota 𝑡 ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) )
25 13 24 nfcxfr 𝑡 𝐶
26 nfcv 𝑡 𝐹
27 25 26 nfne 𝑡 𝐶𝐹
28 27 a1i ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → Ⅎ 𝑡 𝐶𝐹 )
29 13 a1i ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝐶 = ( 𝑦𝐵𝑡𝐴 ( ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) → 𝑦 = 𝑌 ) ) )
30 neeq1 ( 𝑌 = 𝐶 → ( 𝑌𝐹𝐶𝐹 ) )
31 30 adantl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ 𝑌 = 𝐶 ) → ( 𝑌𝐹𝐶𝐹 ) )
32 simpl1 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
33 simpl2 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) )
34 simpl3l ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) )
35 simprl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → 𝑡𝐴 )
36 simprrl ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑡 𝑊 )
37 simprrr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑡 ( 𝑃 𝑄 ) )
38 35 36 37 jca31 ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝑡𝐴 ∧ ¬ 𝑡 𝑊 ) ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) )
39 simp3r1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑣𝐴 )
40 simp3r2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑣 𝑊 )
41 simp3r3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑣 ( 𝑃 𝑄 ) )
42 39 40 41 jca31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ) ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) )
43 42 adantr ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ) ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) )
44 2 3 4 5 6 7 8 12 14 15 cdleme39n ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( ( 𝑡𝐴 ∧ ¬ 𝑡 𝑊 ) ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ∧ ( ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ) ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑌𝐹 )
45 32 33 34 38 43 44 syl113anc ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) ) → 𝑌𝐹 )
46 45 ex ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝑡𝐴 ∧ ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) ) → 𝑌𝐹 ) )
47 simp1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) )
48 simp22r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ¬ 𝑅 𝑊 )
49 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑃𝑄 )
50 1 2 3 4 5 6 7 8 12 13 cdleme25cl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ) ) → 𝐶𝐵 )
51 47 16 48 49 17 50 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝐶𝐵 )
52 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
53 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
54 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) )
55 2 3 5 6 cdlemb2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ 𝑃𝑄 ) → ∃ 𝑡𝐴 ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) )
56 52 53 54 49 55 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → ∃ 𝑡𝐴 ( ¬ 𝑡 𝑊 ∧ ¬ 𝑡 ( 𝑃 𝑄 ) ) )
57 21 28 29 31 46 51 56 riotasv3d ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) ∧ 𝐵 ∈ V ) → 𝐶𝐹 )
58 20 57 mpan2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝐶𝐹 )
59 19 58 eqnetrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ∧ ( 𝑆𝐴 ∧ ¬ 𝑆 𝑊 ) ) ∧ ( ( 𝑅 ( 𝑃 𝑄 ) ∧ 𝑆 ( 𝑃 𝑄 ) ∧ 𝑅𝑆 ) ∧ ( 𝑣𝐴 ∧ ¬ 𝑣 𝑊 ∧ ¬ 𝑣 ( 𝑃 𝑄 ) ) ) ) → 𝑅 / 𝑠 𝑁𝐹 )