This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihopelvalcpre

Description: Member of value of isomorphism H for a lattice K when -. X .<_ W , given auxiliary atom Q . TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014)

Ref Expression
Hypotheses dihopelvalcp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihopelvalcp.l ⊢ ≤ = ( le ‘ 𝐾 )
dihopelvalcp.j ⊢ ∨ = ( join ‘ 𝐾 )
dihopelvalcp.m ⊢ ∧ = ( meet ‘ 𝐾 )
dihopelvalcp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dihopelvalcp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihopelvalcp.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.g ⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
dihopelvalcp.f ⊢ 𝐹 ∈ V
dihopelvalcp.s ⊢ 𝑆 ∈ V
dihopelvalcp.z ⊢ 𝑍 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
dihopelvalcp.n ⊢ 𝑁 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.c ⊢ 𝐶 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihopelvalcp.d ⊢ + = ( +g ‘ 𝑈 )
dihopelvalcp.v ⊢ 𝑉 = ( LSubSp ‘ 𝑈 )
dihopelvalcp.y ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihopelvalcp.o ⊢ 𝑂 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( ℎ ∈ 𝑇 ↦ ( ( 𝑎 ‘ ℎ ) ∘ ( 𝑏 ‘ ℎ ) ) ) )
Assertion dihopelvalcpre ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 dihopelvalcp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihopelvalcp.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dihopelvalcp.j ⊢ ∨ = ( join ‘ 𝐾 )
4 dihopelvalcp.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 dihopelvalcp.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 dihopelvalcp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7 dihopelvalcp.p ⊢ 𝑃 = ( ( oc ‘ 𝐾 ) ‘ 𝑊 )
8 dihopelvalcp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
9 dihopelvalcp.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
10 dihopelvalcp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
11 dihopelvalcp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
12 dihopelvalcp.g ⊢ 𝐺 = ( ℩ 𝑔 ∈ 𝑇 ( 𝑔 ‘ 𝑃 ) = 𝑄 )
13 dihopelvalcp.f ⊢ 𝐹 ∈ V
14 dihopelvalcp.s ⊢ 𝑆 ∈ V
15 dihopelvalcp.z ⊢ 𝑍 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
16 dihopelvalcp.n ⊢ 𝑁 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
17 dihopelvalcp.c ⊢ 𝐶 = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
18 dihopelvalcp.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
19 dihopelvalcp.d ⊢ + = ( +g ‘ 𝑈 )
20 dihopelvalcp.v ⊢ 𝑉 = ( LSubSp ‘ 𝑈 )
21 dihopelvalcp.y ⊢ ⊕ = ( LSSum ‘ 𝑈 )
22 dihopelvalcp.o ⊢ 𝑂 = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( ℎ ∈ 𝑇 ↦ ( ( 𝑎 ‘ ℎ ) ∘ ( 𝑏 ‘ ℎ ) ) ) )
23 1 2 3 4 5 6 11 16 17 18 21 dihvalcq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( 𝐶 ‘ 𝑄 ) ⊕ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) )
24 23 eleq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐶 ‘ 𝑄 ) ⊕ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ) )
25 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
26 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
27 2 5 6 18 17 20 diclss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( 𝐶 ‘ 𝑄 ) ∈ 𝑉 )
28 25 26 27 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝐶 ‘ 𝑄 ) ∈ 𝑉 )
29 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ HL )
30 29 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝐾 ∈ Lat )
31 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑋 ∈ 𝐵 )
32 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐻 )
33 1 6 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
34 32 33 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → 𝑊 ∈ 𝐵 )
35 1 4 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
36 30 31 34 35 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
37 1 2 4 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
38 30 31 34 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 )
39 1 2 6 18 16 20 diblss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝑉 )
40 25 36 38 39 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝑉 )
41 6 18 19 20 21 dvhopellsm ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐶 ‘ 𝑄 ) ∈ 𝑉 ∧ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ∈ 𝑉 ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐶 ‘ 𝑄 ) ⊕ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
42 25 28 40 41 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( ( 𝐶 ‘ 𝑄 ) ⊕ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
43 vex ⊢ 𝑥 ∈ V
44 vex ⊢ 𝑦 ∈ V
45 2 5 6 7 8 10 17 12 43 44 dicopelval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ↔ ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ) )
46 25 26 45 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ↔ ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ) )
47 1 2 6 8 9 15 16 dibopelval3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑊 ) ≤ 𝑊 ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) )
48 25 36 38 47 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ↔ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) )
49 46 48 anbi12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ↔ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) )
50 49 anbi1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ) )
51 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
52 simprll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑥 = ( 𝑦 ‘ 𝐺 ) )
53 simprlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑦 ∈ 𝐸 )
54 2 5 6 7 lhpocnel2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
55 51 54 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
56 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
57 2 5 6 8 12 ltrniotacl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) → 𝐺 ∈ 𝑇 )
58 51 55 56 57 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝐺 ∈ 𝑇 )
59 6 8 10 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑦 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑦 ‘ 𝐺 ) ∈ 𝑇 )
60 51 53 58 59 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑦 ‘ 𝐺 ) ∈ 𝑇 )
61 52 60 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑥 ∈ 𝑇 )
62 simprll ⊢ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) → 𝑧 ∈ 𝑇 )
63 62 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑧 ∈ 𝑇 )
64 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑤 = 𝑍 )
65 1 6 8 10 15 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑍 ∈ 𝐸 )
66 51 65 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑍 ∈ 𝐸 )
67 64 66 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑤 ∈ 𝐸 )
68 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
69 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) )
70 6 8 10 18 68 19 69 dvhopvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑧 ∈ 𝑇 ∧ 𝑤 ∈ 𝐸 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑤 ) ⟩ )
71 51 61 53 63 67 70 syl122anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑤 ) ⟩ )
72 6 8 10 18 68 22 69 dvhfplusr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = 𝑂 )
73 51 72 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = 𝑂 )
74 73 oveqd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑤 ) = ( 𝑦 𝑂 𝑤 ) )
75 74 opeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑤 ) ⟩ = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 𝑂 𝑤 ) ⟩ )
76 71 75 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 𝑂 𝑤 ) ⟩ )
77 76 eqeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ⟨ 𝐹 , 𝑆 ⟩ = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 𝑂 𝑤 ) ⟩ ) )
78 13 14 opth ⊢ ( ⟨ 𝐹 , 𝑆 ⟩ = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 𝑂 𝑤 ) ⟩ ↔ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = ( 𝑦 𝑂 𝑤 ) ) )
79 64 oveq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑦 𝑂 𝑤 ) = ( 𝑦 𝑂 𝑍 ) )
80 1 6 8 10 15 22 tendo0plr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑦 ∈ 𝐸 ) → ( 𝑦 𝑂 𝑍 ) = 𝑦 )
81 51 53 80 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑦 𝑂 𝑍 ) = 𝑦 )
82 79 81 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑦 𝑂 𝑤 ) = 𝑦 )
83 82 eqeq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑆 = ( 𝑦 𝑂 𝑤 ) ↔ 𝑆 = 𝑦 ) )
84 83 anbi2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = ( 𝑦 𝑂 𝑤 ) ) ↔ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) )
85 78 84 bitrid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ⟨ ( 𝑥 ∘ 𝑧 ) , ( 𝑦 𝑂 𝑤 ) ⟩ ↔ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) )
86 77 85 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) )
87 86 pm5.32da ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) )
88 simplll ⊢ ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) → 𝑥 = ( 𝑦 ‘ 𝐺 ) )
89 88 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑥 = ( 𝑦 ‘ 𝐺 ) )
90 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑆 = 𝑦 )
91 90 fveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑆 ‘ 𝐺 ) = ( 𝑦 ‘ 𝐺 ) )
92 89 91 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑥 = ( 𝑆 ‘ 𝐺 ) )
93 90 eqcomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑦 = 𝑆 )
94 coass ⊢ ( ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ∘ 𝑧 ) = ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) )
95 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
96 simpllr ⊢ ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) → 𝑦 ∈ 𝐸 )
97 96 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑦 ∈ 𝐸 )
98 90 97 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑆 ∈ 𝐸 )
99 58 adantrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐺 ∈ 𝑇 )
100 6 8 10 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
101 95 98 99 100 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
102 1 6 8 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ) → ( 𝑆 ‘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 )
103 95 101 102 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑆 ‘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 )
104 f1ococnv1 ⊢ ( ( 𝑆 ‘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 → ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) )
105 103 104 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) )
106 105 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ∘ 𝑧 ) = ( ( I ↾ 𝐵 ) ∘ 𝑧 ) )
107 62 ad2antrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑧 ∈ 𝑇 )
108 1 6 8 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝑇 ) → 𝑧 : 𝐵 –1-1-onto→ 𝐵 )
109 95 107 108 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑧 : 𝐵 –1-1-onto→ 𝐵 )
110 f1of ⊢ ( 𝑧 : 𝐵 –1-1-onto→ 𝐵 → 𝑧 : 𝐵 ⟶ 𝐵 )
111 fcoi2 ⊢ ( 𝑧 : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝑧 ) = 𝑧 )
112 109 110 111 3syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( ( I ↾ 𝐵 ) ∘ 𝑧 ) = 𝑧 )
113 106 112 eqtr2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑧 = ( ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ∘ 𝑧 ) )
114 simprrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐹 = ( 𝑥 ∘ 𝑧 ) )
115 92 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑥 ∘ 𝑧 ) = ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) )
116 114 115 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐹 = ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) )
117 116 coeq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) )
118 6 8 ltrncnv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ) → ◡ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
119 95 101 118 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ◡ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
120 6 8 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ∈ 𝑇 )
121 95 101 107 120 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ∈ 𝑇 )
122 6 8 ltrncom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ◡ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ∧ ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ∈ 𝑇 ) → ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ) = ( ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) )
123 95 119 121 122 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ) = ( ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) )
124 117 123 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) = ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( ( 𝑆 ‘ 𝐺 ) ∘ 𝑧 ) ) )
125 94 113 124 3eqtr4a ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) )
126 simplrr ⊢ ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) → 𝑤 = 𝑍 )
127 126 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑤 = 𝑍 )
128 125 127 jca ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) )
129 92 93 128 jca31 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) )
130 129 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) → ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) )
131 130 pm4.71rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ↔ ( ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) ) )
132 87 131 bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) ) )
133 simprrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐹 = ( 𝑥 ∘ 𝑧 ) )
134 simpll1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
135 88 adantl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑥 = ( 𝑦 ‘ 𝐺 ) )
136 96 adantl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑦 ∈ 𝐸 )
137 134 54 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
138 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
139 138 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
140 134 137 139 57 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐺 ∈ 𝑇 )
141 134 136 140 59 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑦 ‘ 𝐺 ) ∈ 𝑇 )
142 135 141 eqeltrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑥 ∈ 𝑇 )
143 62 ad2antrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑧 ∈ 𝑇 )
144 6 8 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇 ) → ( 𝑥 ∘ 𝑧 ) ∈ 𝑇 )
145 134 142 143 144 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑥 ∘ 𝑧 ) ∈ 𝑇 )
146 133 145 eqeltrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐹 ∈ 𝑇 )
147 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝐾 ∈ HL )
148 147 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐾 ∈ HL )
149 148 hllatd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝐾 ∈ Lat )
150 1 6 8 9 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑧 ) ∈ 𝐵 )
151 134 143 150 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑅 ‘ 𝑧 ) ∈ 𝐵 )
152 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑋 ∈ 𝐵 )
153 152 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑋 ∈ 𝐵 )
154 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑊 ∈ 𝐻 )
155 154 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑊 ∈ 𝐻 )
156 155 33 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → 𝑊 ∈ 𝐵 )
157 149 153 156 35 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑋 ∧ 𝑊 ) ∈ 𝐵 )
158 simprlr ⊢ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) → ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) )
159 158 ad2antrl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) )
160 1 2 4 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑋 )
161 149 153 156 160 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑋 ∧ 𝑊 ) ≤ 𝑋 )
162 1 2 149 151 157 153 159 161 lattrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 )
163 146 136 162 jca31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) → ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) )
164 simprll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑥 = ( 𝑆 ‘ 𝐺 ) )
165 164 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑥 = ( 𝑆 ‘ 𝐺 ) )
166 simprlr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑦 = 𝑆 )
167 166 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑦 = 𝑆 )
168 167 fveq1d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑦 ‘ 𝐺 ) = ( 𝑆 ‘ 𝐺 ) )
169 165 168 eqtr4d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑥 = ( 𝑦 ‘ 𝐺 ) )
170 simprlr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑦 ∈ 𝐸 )
171 169 170 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) )
172 simprrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) )
173 172 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) )
174 simpll1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
175 simprll ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐹 ∈ 𝑇 )
176 167 170 eqeltrrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑆 ∈ 𝐸 )
177 174 54 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
178 138 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) )
179 174 177 178 57 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐺 ∈ 𝑇 )
180 174 176 179 100 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
181 174 180 118 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ◡ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 )
182 6 8 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ◡ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ) → ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∈ 𝑇 )
183 174 175 181 182 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∈ 𝑇 )
184 173 183 eqeltrd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑧 ∈ 𝑇 )
185 simprr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 )
186 2 6 8 9 trlle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑧 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑧 ) ≤ 𝑊 )
187 174 184 186 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑅 ‘ 𝑧 ) ≤ 𝑊 )
188 147 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐾 ∈ HL )
189 188 hllatd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐾 ∈ Lat )
190 174 184 150 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑅 ‘ 𝑧 ) ∈ 𝐵 )
191 152 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑋 ∈ 𝐵 )
192 154 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑊 ∈ 𝐻 )
193 192 33 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑊 ∈ 𝐵 )
194 1 2 4 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ 𝑧 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) ) → ( ( ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑊 ) ↔ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) )
195 189 190 191 193 194 syl13anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( ( ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑊 ) ↔ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) )
196 185 187 195 mpbi2and ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) )
197 simprrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → 𝑤 = 𝑍 )
198 197 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑤 = 𝑍 )
199 184 196 198 jca31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) )
200 174 180 102 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑆 ‘ 𝐺 ) : 𝐵 –1-1-onto→ 𝐵 )
201 200 104 syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) = ( I ↾ 𝐵 ) )
202 201 coeq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝐹 ∘ ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) = ( 𝐹 ∘ ( I ↾ 𝐵 ) ) )
203 1 6 8 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
204 174 175 203 syl2anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
205 f1of ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → 𝐹 : 𝐵 ⟶ 𝐵 )
206 fcoi1 ⊢ ( 𝐹 : 𝐵 ⟶ 𝐵 → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
207 204 205 206 3syl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝐹 ∘ ( I ↾ 𝐵 ) ) = 𝐹 )
208 202 207 eqtr2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐹 = ( 𝐹 ∘ ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) ) )
209 coass ⊢ ( ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∘ ( 𝑆 ‘ 𝐺 ) ) = ( 𝐹 ∘ ( ◡ ( 𝑆 ‘ 𝐺 ) ∘ ( 𝑆 ‘ 𝐺 ) ) )
210 208 209 eqtr4di ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐹 = ( ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∘ ( 𝑆 ‘ 𝐺 ) ) )
211 6 8 ltrncom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑆 ‘ 𝐺 ) ∈ 𝑇 ∧ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∈ 𝑇 ) → ( ( 𝑆 ‘ 𝐺 ) ∘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) = ( ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∘ ( 𝑆 ‘ 𝐺 ) ) )
212 174 180 183 211 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( ( 𝑆 ‘ 𝐺 ) ∘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) = ( ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∘ ( 𝑆 ‘ 𝐺 ) ) )
213 210 212 eqtr4d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐹 = ( ( 𝑆 ‘ 𝐺 ) ∘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) )
214 165 173 coeq12d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝑥 ∘ 𝑧 ) = ( ( 𝑆 ‘ 𝐺 ) ∘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) )
215 213 214 eqtr4d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝐹 = ( 𝑥 ∘ 𝑧 ) )
216 167 eqcomd ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → 𝑆 = 𝑦 )
217 215 216 jca ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) )
218 171 199 217 jca31 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) → ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) )
219 163 218 impbida ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) ∧ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ) → ( ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) )
220 219 pm5.32da ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) ↔ ( ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) ) )
221 df-3an ⊢ ( ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) ↔ ( ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) )
222 220 221 bitr4di ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( ( ( 𝑥 = ( 𝑦 ‘ 𝐺 ) ∧ 𝑦 ∈ 𝐸 ) ∧ ( ( 𝑧 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑧 ) ≤ ( 𝑋 ∧ 𝑊 ) ) ∧ 𝑤 = 𝑍 ) ) ∧ ( 𝐹 = ( 𝑥 ∘ 𝑧 ) ∧ 𝑆 = 𝑦 ) ) ) ↔ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) ) )
223 50 132 222 3bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) ) )
224 223 4exbidv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) ) )
225 fvex ⊢ ( 𝑆 ‘ 𝐺 ) ∈ V
226 225 cnvex ⊢ ◡ ( 𝑆 ‘ 𝐺 ) ∈ V
227 13 226 coex ⊢ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∈ V
228 8 fvexi ⊢ 𝑇 ∈ V
229 228 mptex ⊢ ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) ) ∈ V
230 15 229 eqeltri ⊢ 𝑍 ∈ V
231 biidd ⊢ ( 𝑥 = ( 𝑆 ‘ 𝐺 ) → ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) )
232 eleq1 ⊢ ( 𝑦 = 𝑆 → ( 𝑦 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸 ) )
233 232 anbi2d ⊢ ( 𝑦 = 𝑆 → ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ↔ ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) )
234 233 anbi1d ⊢ ( 𝑦 = 𝑆 → ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) )
235 fveq2 ⊢ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) )
236 235 breq1d ⊢ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) → ( ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ↔ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) )
237 236 anbi2d ⊢ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) → ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )
238 biidd ⊢ ( 𝑤 = 𝑍 → ( ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )
239 225 14 227 230 231 234 237 238 ceqsex4v ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ( 𝑆 ‘ 𝐺 ) ∧ 𝑦 = 𝑆 ) ∧ ( 𝑧 = ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ∧ 𝑤 = 𝑍 ) ∧ ( ( 𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸 ) ∧ ( 𝑅 ‘ 𝑧 ) ≤ 𝑋 ) ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) )
240 224 239 bitrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐶 ‘ 𝑄 ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑁 ‘ ( 𝑋 ∧ 𝑊 ) ) ) ∧ ⟨ 𝐹 , 𝑆 ⟩ = ( ⟨ 𝑥 , 𝑦 ⟩ + ⟨ 𝑧 , 𝑤 ⟩ ) ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )
241 24 42 240 3bitrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ∧ ( 𝑄 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) ) → ( ⟨ 𝐹 , 𝑆 ⟩ ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ∧ ( 𝑅 ‘ ( 𝐹 ∘ ◡ ( 𝑆 ‘ 𝐺 ) ) ) ≤ 𝑋 ) ) )