Metamath Proof Explorer


Theorem cdlemk27-3

Description: Part of proof of Lemma K of Crawley p. 118. Eliminate the P from the conclusion of cdlemk25-3 . (Contributed by NM, 10-Jul-2013)

Ref Expression
Hypotheses cdlemk3.b 𝐵 = ( Base ‘ 𝐾 )
cdlemk3.l = ( le ‘ 𝐾 )
cdlemk3.j = ( join ‘ 𝐾 )
cdlemk3.m = ( meet ‘ 𝐾 )
cdlemk3.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemk3.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemk3.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemk3.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemk3.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
cdlemk3.u1 𝑌 = ( 𝑑𝑇 , 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( ( 𝑆𝑑 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑒 𝑑 ) ) ) ) ) )
Assertion cdlemk27-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐷 𝑌 𝐺 ) = ( 𝐶 𝑌 𝐺 ) )

Proof

Step Hyp Ref Expression
1 cdlemk3.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemk3.l = ( le ‘ 𝐾 )
3 cdlemk3.j = ( join ‘ 𝐾 )
4 cdlemk3.m = ( meet ‘ 𝐾 )
5 cdlemk3.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemk3.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemk3.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemk3.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemk3.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
10 cdlemk3.u1 𝑌 = ( 𝑑𝑇 , 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( ( 𝑆𝑑 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑒 𝑑 ) ) ) ) ) )
11 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
12 simp221 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
13 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝐺𝑇 )
14 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) )
15 simp3l3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) )
16 simp3r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) )
17 16 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) )
18 15 17 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) ) )
19 simp222 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
20 simp23l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
21 simp223 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝐷 ≠ ( I ↾ 𝐵 ) )
22 19 20 21 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) )
23 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
24 1 2 3 4 5 6 7 8 9 10 cdlemkuel-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐺𝑇 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( 𝐷 𝑌 𝐺 ) ∈ 𝑇 )
25 11 12 13 14 18 22 23 24 syl313anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐷 𝑌 𝐺 ) ∈ 𝑇 )
26 simp121 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝐹𝑇 )
27 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝐶𝑇 )
28 simp123 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝑁𝑇 )
29 simp3l2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) )
30 simp3l1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) )
31 30 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝑅𝐶 ) ≠ ( 𝑅𝐺 ) )
32 29 31 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐺 ) ) )
33 simp23r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → 𝐶 ≠ ( I ↾ 𝐵 ) )
34 19 20 33 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) )
35 1 2 3 4 5 6 7 8 9 10 cdlemkuel-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐺𝑇 ) ∧ ( 𝐹𝑇𝐶𝑇𝑁𝑇 ) ∧ ( ( ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ) → ( 𝐶 𝑌 𝐺 ) ∈ 𝑇 )
36 11 12 13 26 27 28 32 34 23 35 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐶 𝑌 𝐺 ) ∈ 𝑇 )
37 1 2 3 4 5 6 7 8 9 10 cdlemk26-3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( ( 𝐷 𝑌 𝐺 ) ‘ 𝑃 ) = ( ( 𝐶 𝑌 𝐺 ) ‘ 𝑃 ) )
38 2 5 6 7 cdlemd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐷 𝑌 𝐺 ) ∈ 𝑇 ∧ ( 𝐶 𝑌 𝐺 ) ∈ 𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝐷 𝑌 𝐺 ) ‘ 𝑃 ) = ( ( 𝐶 𝑌 𝐺 ) ‘ 𝑃 ) ) → ( 𝐷 𝑌 𝐺 ) = ( 𝐶 𝑌 𝐺 ) )
39 11 25 36 23 37 38 syl311anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐷𝑇𝑁𝑇 ) ∧ ( 𝐺𝑇𝐶𝑇 ) ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐷 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺 ≠ ( I ↾ 𝐵 ) ∧ 𝐶 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( ( ( 𝑅𝐺 ) ≠ ( 𝑅𝐶 ) ∧ ( 𝑅𝐶 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐷 ) ≠ ( 𝑅𝐹 ) ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝐷 ) ) ) → ( 𝐷 𝑌 𝐺 ) = ( 𝐶 𝑌 𝐺 ) )