Metamath Proof Explorer


Theorem cdlemk11ta

Description: Part of proof of Lemma K of Crawley p. 118. Lemma for Eq. 5, p. 119. G , I stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b 𝐵 = ( Base ‘ 𝐾 )
cdlemk5.l = ( le ‘ 𝐾 )
cdlemk5.j = ( join ‘ 𝐾 )
cdlemk5.m = ( meet ‘ 𝐾 )
cdlemk5.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemk5.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemk5.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemk5.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemk5.z 𝑍 = ( ( 𝑃 ( 𝑅𝑏 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑏 𝐹 ) ) ) )
cdlemk5.y 𝑌 = ( ( 𝑃 ( 𝑅𝑔 ) ) ( 𝑍 ( 𝑅 ‘ ( 𝑔 𝑏 ) ) ) )
cdlemk5c.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
cdlemk5a.u2 𝐶 = ( 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( ( 𝑆𝑏 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑒 𝑏 ) ) ) ) ) )
Assertion cdlemk11ta ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐺 / 𝑔 𝑌 ( 𝐼 / 𝑔 𝑌 ( 𝑅 ‘ ( 𝐼 𝐺 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdlemk5.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemk5.l = ( le ‘ 𝐾 )
3 cdlemk5.j = ( join ‘ 𝐾 )
4 cdlemk5.m = ( meet ‘ 𝐾 )
5 cdlemk5.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemk5.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemk5.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemk5.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemk5.z 𝑍 = ( ( 𝑃 ( 𝑅𝑏 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑏 𝐹 ) ) ) )
10 cdlemk5.y 𝑌 = ( ( 𝑃 ( 𝑅𝑔 ) ) ( 𝑍 ( 𝑅 ‘ ( 𝑔 𝑏 ) ) ) )
11 cdlemk5c.s 𝑆 = ( 𝑓𝑇 ↦ ( 𝑖𝑇 ( 𝑖𝑃 ) = ( ( 𝑃 ( 𝑅𝑓 ) ) ( ( 𝑁𝑃 ) ( 𝑅 ‘ ( 𝑓 𝐹 ) ) ) ) ) )
12 cdlemk5a.u2 𝐶 = ( 𝑒𝑇 ↦ ( 𝑗𝑇 ( 𝑗𝑃 ) = ( ( 𝑃 ( 𝑅𝑒 ) ) ( ( ( 𝑆𝑏 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝑒 𝑏 ) ) ) ) ) )
13 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
14 simp12l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐹𝑇 )
15 simp31 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝑏𝑇 )
16 simp21 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝑁𝑇 )
17 simp13l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐺𝑇 )
18 simp331 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐼𝑇 )
19 16 17 18 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑁𝑇𝐺𝑇𝐼𝑇 ) )
20 simp22 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
21 simp23 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑅𝐹 ) = ( 𝑅𝑁 ) )
22 simp12r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
23 simp321 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝑏 ≠ ( I ↾ 𝐵 ) )
24 simp13r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐺 ≠ ( I ↾ 𝐵 ) )
25 22 23 24 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑏 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) )
26 simp332 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐼 ≠ ( I ↾ 𝐵 ) )
27 simp322 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) )
28 simp323 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) )
29 28 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑅𝐺 ) ≠ ( 𝑅𝑏 ) )
30 simp333 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) )
31 30 necomd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑅𝐼 ) ≠ ( 𝑅𝑏 ) )
32 27 29 31 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑏 ) ∧ ( 𝑅𝐼 ) ≠ ( 𝑅𝑏 ) ) )
33 eqid ( 𝑆𝑏 ) = ( 𝑆𝑏 )
34 eqid ( ( ( 𝐺𝑃 ) ( 𝐼𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝑏 ) ) ( 𝑅 ‘ ( 𝐼 𝑏 ) ) ) ) = ( ( ( 𝐺𝑃 ) ( 𝐼𝑃 ) ) ( ( 𝑅 ‘ ( 𝐺 𝑏 ) ) ( 𝑅 ‘ ( 𝐼 𝑏 ) ) ) )
35 1 2 3 4 5 6 7 8 11 33 12 34 cdlemk11u ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝑏𝑇 ) ∧ ( ( 𝑁𝑇𝐺𝑇𝐼𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝑏 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ) ∧ 𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝐺 ) ≠ ( 𝑅𝑏 ) ∧ ( 𝑅𝐼 ) ≠ ( 𝑅𝑏 ) ) ) ) → ( ( 𝐶𝐺 ) ‘ 𝑃 ) ( ( ( 𝐶𝐼 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝐼 𝐺 ) ) ) )
36 13 14 15 19 20 21 25 26 32 35 syl333anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( ( 𝐶𝐺 ) ‘ 𝑃 ) ( ( ( 𝐶𝐼 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝐼 𝐺 ) ) ) )
37 simp32 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) )
38 15 37 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) )
39 1 2 3 4 5 6 7 8 9 10 11 12 cdlemkyuu ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ) ) → 𝐺 / 𝑔 𝑌 = ( ( 𝐶𝐺 ) ‘ 𝑃 ) )
40 38 39 syld3an3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐺 / 𝑔 𝑌 = ( ( 𝐶𝐺 ) ‘ 𝑃 ) )
41 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) )
42 18 26 jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ) )
43 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) )
44 23 27 30 3jca ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 cdlemkyuu ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐼 / 𝑔 𝑌 = ( ( 𝐶𝐼 ) ‘ 𝑃 ) )
46 13 41 42 43 15 44 45 syl312anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐼 / 𝑔 𝑌 = ( ( 𝐶𝐼 ) ‘ 𝑃 ) )
47 46 oveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → ( 𝐼 / 𝑔 𝑌 ( 𝑅 ‘ ( 𝐼 𝐺 ) ) ) = ( ( ( 𝐶𝐼 ) ‘ 𝑃 ) ( 𝑅 ‘ ( 𝐼 𝐺 ) ) ) )
48 36 40 47 3brtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝐺𝑇𝐺 ≠ ( I ↾ 𝐵 ) ) ) ∧ ( 𝑁𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐹 ) = ( 𝑅𝑁 ) ) ∧ ( 𝑏𝑇 ∧ ( 𝑏 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐹 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐺 ) ) ∧ ( 𝐼𝑇𝐼 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅𝑏 ) ≠ ( 𝑅𝐼 ) ) ) ) → 𝐺 / 𝑔 𝑌 ( 𝐼 / 𝑔 𝑌 ( 𝑅 ‘ ( 𝐼 𝐺 ) ) ) )