Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihopelvalcpre Structured version   Visualization version   GIF version

Theorem dihopelvalcpre 37136
Description: Member of value of isomorphism H for a lattice 𝐾 when ¬ 𝑋 𝑊, given auxiliary atom 𝑄. TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014.)
Hypotheses
Ref Expression
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
Ref Expression
dihopelvalcpre (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼𝑋) ↔ ((𝐹𝑇𝑆𝐸) ∧ (𝑅‘(𝐹(𝑆𝐺))) 𝑋)))
Distinct variable groups:   ,𝑔   𝐴,𝑔   𝑃,𝑔   𝑎,𝑏,𝐸   𝑔,,𝐻   𝑔,𝑎,,𝐾,𝑏   𝐵,   𝑇,𝑎,𝑏,𝑔,   𝑊,𝑎,𝑏,𝑔,   𝑄,𝑔
Allowed substitution hints:   𝐴(,𝑎,𝑏)   𝐵(𝑔,𝑎,𝑏)   𝐶(𝑔,,𝑎,𝑏)   𝑃(,𝑎,𝑏)   + (𝑔,,𝑎,𝑏)   (𝑔,,𝑎,𝑏)   𝑄(,𝑎,𝑏)   𝑅(𝑔,,𝑎,𝑏)   𝑆(𝑔,,𝑎,𝑏)   𝑈(𝑔,,𝑎,𝑏)   𝐸(𝑔,)   𝐹(𝑔,,𝑎,𝑏)   𝐺(𝑔,,𝑎,𝑏)   𝐻(𝑎,𝑏)   𝐼(𝑔,,𝑎,𝑏)   (𝑔,,𝑎,𝑏)   (,𝑎,𝑏)   (𝑔,,𝑎,𝑏)   𝑁(𝑔,,𝑎,𝑏)   𝑂(𝑔,,𝑎,𝑏)   𝑉(𝑔,,𝑎,𝑏)   𝑋(𝑔,,𝑎,𝑏)   𝑍(𝑔,,𝑎,𝑏)

Proof of Theorem dihopelvalcpre
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dihopelvalcp.b . . . 4 𝐵 = (Base‘𝐾)
2 dihopelvalcp.l . . . 4 = (le‘𝐾)
3 dihopelvalcp.j . . . 4 = (join‘𝐾)
4 dihopelvalcp.m . . . 4 = (meet‘𝐾)
5 dihopelvalcp.a . . . 4 𝐴 = (Atoms‘𝐾)
6 dihopelvalcp.h . . . 4 𝐻 = (LHyp‘𝐾)
7 dihopelvalcp.i . . . 4 𝐼 = ((DIsoH‘𝐾)‘𝑊)
8 dihopelvalcp.n . . . 4 𝑁 = ((DIsoB‘𝐾)‘𝑊)
9 dihopelvalcp.c . . . 4 𝐶 = ((DIsoC‘𝐾)‘𝑊)
10 dihopelvalcp.u . . . 4 𝑈 = ((DVecH‘𝐾)‘𝑊)
11 dihopelvalcp.y . . . 4 = (LSSum‘𝑈)
121, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11dihvalcq 37124 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (𝐼𝑋) = ((𝐶𝑄) (𝑁‘(𝑋 𝑊))))
1312eleq2d 2830 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼𝑋) ↔ ⟨𝐹, 𝑆⟩ ∈ ((𝐶𝑄) (𝑁‘(𝑋 𝑊)))))
14 simp1 1166 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
15 simp3l 1258 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
16 dihopelvalcp.v . . . . 5 𝑉 = (LSubSp‘𝑈)
172, 5, 6, 10, 9, 16diclss 37081 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (𝐶𝑄) ∈ 𝑉)
1814, 15, 17syl2anc 579 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (𝐶𝑄) ∈ 𝑉)
19 simp1l 1254 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
2019hllatd 35252 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
21 simp2l 1256 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → 𝑋𝐵)
22 simp1r 1255 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → 𝑊𝐻)
231, 6lhpbase 35886 . . . . . 6 (𝑊𝐻𝑊𝐵)
2422, 23syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → 𝑊𝐵)
251, 4latmcl 17320 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋 𝑊) ∈ 𝐵)
2620, 21, 24, 25syl3anc 1490 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (𝑋 𝑊) ∈ 𝐵)
271, 2, 4latmle2 17345 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋 𝑊) 𝑊)
2820, 21, 24, 27syl3anc 1490 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (𝑋 𝑊) 𝑊)
291, 2, 6, 10, 8, 16diblss 37058 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑋 𝑊) ∈ 𝐵 ∧ (𝑋 𝑊) 𝑊)) → (𝑁‘(𝑋 𝑊)) ∈ 𝑉)
3014, 26, 28, 29syl12anc 865 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (𝑁‘(𝑋 𝑊)) ∈ 𝑉)
31 dihopelvalcp.d . . . 4 + = (+g𝑈)
326, 10, 31, 16, 11dvhopellsm 37005 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐶𝑄) ∈ 𝑉 ∧ (𝑁‘(𝑋 𝑊)) ∈ 𝑉) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶𝑄) (𝑁‘(𝑋 𝑊))) ↔ ∃𝑥𝑦𝑧𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩))))
3314, 18, 30, 32syl3anc 1490 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶𝑄) (𝑁‘(𝑋 𝑊))) ↔ ∃𝑥𝑦𝑧𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩))))
34 dihopelvalcp.p . . . . . . . . 9 𝑃 = ((oc‘𝐾)‘𝑊)
35 dihopelvalcp.t . . . . . . . . 9 𝑇 = ((LTrn‘𝐾)‘𝑊)
36 dihopelvalcp.e . . . . . . . . 9 𝐸 = ((TEndo‘𝐾)‘𝑊)
37 dihopelvalcp.g . . . . . . . . 9 𝐺 = (𝑔𝑇 (𝑔𝑃) = 𝑄)
38 vex 3353 . . . . . . . . 9 𝑥 ∈ V
39 vex 3353 . . . . . . . . 9 𝑦 ∈ V
402, 5, 6, 34, 35, 36, 9, 37, 38, 39dicopelval2 37069 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ↔ (𝑥 = (𝑦𝐺) ∧ 𝑦𝐸)))
4114, 15, 40syl2anc 579 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ↔ (𝑥 = (𝑦𝐺) ∧ 𝑦𝐸)))
42 dihopelvalcp.r . . . . . . . . 9 𝑅 = ((trL‘𝐾)‘𝑊)
43 dihopelvalcp.z . . . . . . . . 9 𝑍 = (𝑇 ↦ ( I ↾ 𝐵))
441, 2, 6, 35, 42, 43, 8dibopelval3 37036 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑋 𝑊) ∈ 𝐵 ∧ (𝑋 𝑊) 𝑊)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊)) ↔ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)))
4514, 26, 28, 44syl12anc 865 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊)) ↔ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)))
4641, 45anbi12d 624 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → ((⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊))) ↔ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))))
4746anbi1d 623 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩))))
48 simpl1 1242 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
49 simprll 797 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑦𝐺))
50 simprlr 798 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑦𝐸)
512, 5, 6, 34lhpocnel2 35907 . . . . . . . . . . . . . . 15 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
5248, 51syl 17 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
53 simpl3l 1301 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
542, 5, 6, 35, 37ltrniotacl 36467 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) → 𝐺𝑇)
5548, 52, 53, 54syl3anc 1490 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝐺𝑇)
566, 35, 36tendocl 36655 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑦𝐸𝐺𝑇) → (𝑦𝐺) ∈ 𝑇)
5748, 50, 55, 56syl3anc 1490 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝐺) ∈ 𝑇)
5849, 57eqeltrd 2844 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥𝑇)
59 simprll 797 . . . . . . . . . . . 12 (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) → 𝑧𝑇)
6059adantl 473 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑧𝑇)
61 simprrr 800 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
621, 6, 35, 36, 43tendo0cl 36678 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑍𝐸)
6348, 62syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑍𝐸)
6461, 63eqeltrd 2844 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤𝐸)
65 eqid 2765 . . . . . . . . . . . 12 (Scalar‘𝑈) = (Scalar‘𝑈)
66 eqid 2765 . . . . . . . . . . . 12 (+g‘(Scalar‘𝑈)) = (+g‘(Scalar‘𝑈))
676, 35, 36, 10, 65, 31, 66dvhopvadd 36981 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑥𝑇𝑦𝐸) ∧ (𝑧𝑇𝑤𝐸)) → (⟨𝑥, 𝑦+𝑧, 𝑤⟩) = ⟨(𝑥𝑧), (𝑦(+g‘(Scalar‘𝑈))𝑤)⟩)
6848, 58, 50, 60, 64, 67syl122anc 1498 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦+𝑧, 𝑤⟩) = ⟨(𝑥𝑧), (𝑦(+g‘(Scalar‘𝑈))𝑤)⟩)
69 dihopelvalcp.o . . . . . . . . . . . . . 14 𝑂 = (𝑎𝐸, 𝑏𝐸 ↦ (𝑇 ↦ ((𝑎) ∘ (𝑏))))
706, 35, 36, 10, 65, 69, 66dvhfplusr 36972 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (+g‘(Scalar‘𝑈)) = 𝑂)
7148, 70syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (+g‘(Scalar‘𝑈)) = 𝑂)
7271oveqd 6859 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦(+g‘(Scalar‘𝑈))𝑤) = (𝑦𝑂𝑤))
7372opeq2d 4566 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → ⟨(𝑥𝑧), (𝑦(+g‘(Scalar‘𝑈))𝑤)⟩ = ⟨(𝑥𝑧), (𝑦𝑂𝑤)⟩)
7468, 73eqtrd 2799 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦+𝑧, 𝑤⟩) = ⟨(𝑥𝑧), (𝑦𝑂𝑤)⟩)
7574eqeq2d 2775 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = ⟨(𝑥𝑧), (𝑦𝑂𝑤)⟩))
76 dihopelvalcp.f . . . . . . . . . 10 𝐹 ∈ V
77 dihopelvalcp.s . . . . . . . . . 10 𝑆 ∈ V
7876, 77opth 5100 . . . . . . . . 9 (⟨𝐹, 𝑆⟩ = ⟨(𝑥𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)))
7961oveq2d 6858 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = (𝑦𝑂𝑍))
801, 6, 35, 36, 43, 69tendo0plr 36680 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑦𝐸) → (𝑦𝑂𝑍) = 𝑦)
8148, 50, 80syl2anc 579 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑍) = 𝑦)
8279, 81eqtrd 2799 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = 𝑦)
8382eqeq2d 2775 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑆 = (𝑦𝑂𝑤) ↔ 𝑆 = 𝑦))
8483anbi2d 622 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → ((𝐹 = (𝑥𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)) ↔ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)))
8578, 84syl5bb 274 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = ⟨(𝑥𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)))
8675, 85bitrd 270 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩) ↔ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)))
8786pm5.32da 574 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))))
88 simplll 791 . . . . . . . . . . 11 ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)) → 𝑥 = (𝑦𝐺))
8988adantl 473 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦𝐺))
90 simprrr 800 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 = 𝑦)
9190fveq1d 6377 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑆𝐺) = (𝑦𝐺))
9289, 91eqtr4d 2802 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑆𝐺))
9390eqcomd 2771 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 = 𝑆)
94 coass 5840 . . . . . . . . . . 11 (((𝑆𝐺) ∘ (𝑆𝐺)) ∘ 𝑧) = ((𝑆𝐺) ∘ ((𝑆𝐺) ∘ 𝑧))
95 simpl1 1242 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
96 simpllr 793 . . . . . . . . . . . . . . . . . 18 ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)) → 𝑦𝐸)
9796adantl 473 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑦𝐸)
9890, 97eqeltrd 2844 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑆𝐸)
9955adantrr 708 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐺𝑇)
1006, 35, 36tendocl 36655 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑆𝐸𝐺𝑇) → (𝑆𝐺) ∈ 𝑇)
10195, 98, 99, 100syl3anc 1490 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑆𝐺) ∈ 𝑇)
1021, 6, 35ltrn1o 36012 . . . . . . . . . . . . . . 15 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐺) ∈ 𝑇) → (𝑆𝐺):𝐵1-1-onto𝐵)
10395, 101, 102syl2anc 579 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑆𝐺):𝐵1-1-onto𝐵)
104 f1ococnv1 6348 . . . . . . . . . . . . . 14 ((𝑆𝐺):𝐵1-1-onto𝐵 → ((𝑆𝐺) ∘ (𝑆𝐺)) = ( I ↾ 𝐵))
105103, 104syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆𝐺) ∘ (𝑆𝐺)) = ( I ↾ 𝐵))
106105coeq1d 5452 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (((𝑆𝐺) ∘ (𝑆𝐺)) ∘ 𝑧) = (( I ↾ 𝐵) ∘ 𝑧))
10759ad2antrl 719 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑧𝑇)
1081, 6, 35ltrn1o 36012 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑧𝑇) → 𝑧:𝐵1-1-onto𝐵)
10995, 107, 108syl2anc 579 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑧:𝐵1-1-onto𝐵)
110 f1of 6320 . . . . . . . . . . . . 13 (𝑧:𝐵1-1-onto𝐵𝑧:𝐵𝐵)
111 fcoi2 6261 . . . . . . . . . . . . 13 (𝑧:𝐵𝐵 → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
112109, 110, 1113syl 18 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
113106, 112eqtr2d 2800 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = (((𝑆𝐺) ∘ (𝑆𝐺)) ∘ 𝑧))
114 simprrl 799 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥𝑧))
11592coeq1d 5452 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑥𝑧) = ((𝑆𝐺) ∘ 𝑧))
116114, 115eqtrd 2799 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = ((𝑆𝐺) ∘ 𝑧))
117116coeq1d 5452 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝐹(𝑆𝐺)) = (((𝑆𝐺) ∘ 𝑧) ∘ (𝑆𝐺)))
1186, 35ltrncnv 36034 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐺) ∈ 𝑇) → (𝑆𝐺) ∈ 𝑇)
11995, 101, 118syl2anc 579 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑆𝐺) ∈ 𝑇)
1206, 35ltrnco 36607 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐺) ∈ 𝑇𝑧𝑇) → ((𝑆𝐺) ∘ 𝑧) ∈ 𝑇)
12195, 101, 107, 120syl3anc 1490 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆𝐺) ∘ 𝑧) ∈ 𝑇)
1226, 35ltrncom 36626 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐺) ∈ 𝑇 ∧ ((𝑆𝐺) ∘ 𝑧) ∈ 𝑇) → ((𝑆𝐺) ∘ ((𝑆𝐺) ∘ 𝑧)) = (((𝑆𝐺) ∘ 𝑧) ∘ (𝑆𝐺)))
12395, 119, 121, 122syl3anc 1490 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆𝐺) ∘ ((𝑆𝐺) ∘ 𝑧)) = (((𝑆𝐺) ∘ 𝑧) ∘ (𝑆𝐺)))
124117, 123eqtr4d 2802 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝐹(𝑆𝐺)) = ((𝑆𝐺) ∘ ((𝑆𝐺) ∘ 𝑧)))
12594, 113, 1243eqtr4a 2825 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = (𝐹(𝑆𝐺)))
126 simplrr 796 . . . . . . . . . . 11 ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)) → 𝑤 = 𝑍)
127126adantl 473 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑤 = 𝑍)
128125, 127jca 507 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))
12992, 93, 128jca31 510 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍)))
130129ex 401 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)) → ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))))
131130pm4.71rd 558 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)) ↔ (((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)))))
13287, 131bitrd 270 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)))))
133 simprrl 799 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥𝑧))
134 simpll1 1269 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
13588adantl 473 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦𝐺))
13696adantl 473 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑦𝐸)
137134, 51syl 17 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
138 simpl3l 1301 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
139138adantr 472 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
140134, 137, 139, 54syl3anc 1490 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐺𝑇)
141134, 136, 140, 56syl3anc 1490 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑦𝐺) ∈ 𝑇)
142135, 141eqeltrd 2844 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑥𝑇)
14359ad2antrl 719 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑧𝑇)
1446, 35ltrnco 36607 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑥𝑇𝑧𝑇) → (𝑥𝑧) ∈ 𝑇)
145134, 142, 143, 144syl3anc 1490 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑥𝑧) ∈ 𝑇)
146133, 145eqeltrd 2844 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐹𝑇)
147 simpl1l 1293 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → 𝐾 ∈ HL)
148147adantr 472 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ HL)
149148hllatd 35252 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ Lat)
1501, 6, 35, 42trlcl 36052 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑧𝑇) → (𝑅𝑧) ∈ 𝐵)
151134, 143, 150syl2anc 579 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑅𝑧) ∈ 𝐵)
152 simpl2l 1297 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → 𝑋𝐵)
153152adantr 472 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑋𝐵)
154 simpl1r 1295 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → 𝑊𝐻)
155154adantr 472 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑊𝐻)
156155, 23syl 17 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → 𝑊𝐵)
157149, 153, 156, 25syl3anc 1490 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 𝑊) ∈ 𝐵)
158 simprlr 798 . . . . . . . . . . 11 (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) → (𝑅𝑧) (𝑋 𝑊))
159158ad2antrl 719 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑅𝑧) (𝑋 𝑊))
1601, 2, 4latmle1 17344 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵) → (𝑋 𝑊) 𝑋)
161149, 153, 156, 160syl3anc 1490 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 𝑊) 𝑋)
1621, 2, 149, 151, 157, 153, 159, 161lattrd 17326 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → (𝑅𝑧) 𝑋)
163146, 136, 162jca31 510 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) → ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋))
164 simprll 797 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑆𝐺))
165164adantr 472 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑥 = (𝑆𝐺))
166 simprlr 798 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → 𝑦 = 𝑆)
167166adantr 472 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑦 = 𝑆)
168167fveq1d 6377 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑦𝐺) = (𝑆𝐺))
169165, 168eqtr4d 2802 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑥 = (𝑦𝐺))
170 simprlr 798 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑦𝐸)
171169, 170jca 507 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑥 = (𝑦𝐺) ∧ 𝑦𝐸))
172 simprrl 799 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → 𝑧 = (𝐹(𝑆𝐺)))
173172adantr 472 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑧 = (𝐹(𝑆𝐺)))
174 simpll1 1269 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
175 simprll 797 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐹𝑇)
176167, 170eqeltrrd 2845 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑆𝐸)
177174, 51syl 17 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
178138adantr 472 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
179174, 177, 178, 54syl3anc 1490 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐺𝑇)
180174, 176, 179, 100syl3anc 1490 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑆𝐺) ∈ 𝑇)
181174, 180, 118syl2anc 579 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑆𝐺) ∈ 𝑇)
1826, 35ltrnco 36607 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇(𝑆𝐺) ∈ 𝑇) → (𝐹(𝑆𝐺)) ∈ 𝑇)
183174, 175, 181, 182syl3anc 1490 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝐹(𝑆𝐺)) ∈ 𝑇)
184173, 183eqeltrd 2844 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑧𝑇)
185 simprr 789 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑅𝑧) 𝑋)
1862, 6, 35, 42trlle 36072 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑧𝑇) → (𝑅𝑧) 𝑊)
187174, 184, 186syl2anc 579 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑅𝑧) 𝑊)
188147adantr 472 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐾 ∈ HL)
189188hllatd 35252 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐾 ∈ Lat)
190174, 184, 150syl2anc 579 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑅𝑧) ∈ 𝐵)
191152adantr 472 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑋𝐵)
192154adantr 472 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑊𝐻)
193192, 23syl 17 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑊𝐵)
1941, 2, 4latlem12 17346 . . . . . . . . . . . 12 ((𝐾 ∈ Lat ∧ ((𝑅𝑧) ∈ 𝐵𝑋𝐵𝑊𝐵)) → (((𝑅𝑧) 𝑋 ∧ (𝑅𝑧) 𝑊) ↔ (𝑅𝑧) (𝑋 𝑊)))
195189, 190, 191, 193, 194syl13anc 1491 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (((𝑅𝑧) 𝑋 ∧ (𝑅𝑧) 𝑊) ↔ (𝑅𝑧) (𝑋 𝑊)))
196185, 187, 195mpbi2and 703 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑅𝑧) (𝑋 𝑊))
197 simprrr 800 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
198197adantr 472 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑤 = 𝑍)
199184, 196, 198jca31 510 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍))
200174, 180, 102syl2anc 579 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑆𝐺):𝐵1-1-onto𝐵)
201200, 104syl 17 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → ((𝑆𝐺) ∘ (𝑆𝐺)) = ( I ↾ 𝐵))
202201coeq2d 5453 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝐹 ∘ ((𝑆𝐺) ∘ (𝑆𝐺))) = (𝐹 ∘ ( I ↾ 𝐵)))
2031, 6, 35ltrn1o 36012 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹:𝐵1-1-onto𝐵)
204174, 175, 203syl2anc 579 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐹:𝐵1-1-onto𝐵)
205 f1of 6320 . . . . . . . . . . . . . . 15 (𝐹:𝐵1-1-onto𝐵𝐹:𝐵𝐵)
206 fcoi1 6260 . . . . . . . . . . . . . . 15 (𝐹:𝐵𝐵 → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
207204, 205, 2063syl 18 . . . . . . . . . . . . . 14 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
208202, 207eqtr2d 2800 . . . . . . . . . . . . 13 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐹 = (𝐹 ∘ ((𝑆𝐺) ∘ (𝑆𝐺))))
209 coass 5840 . . . . . . . . . . . . 13 ((𝐹(𝑆𝐺)) ∘ (𝑆𝐺)) = (𝐹 ∘ ((𝑆𝐺) ∘ (𝑆𝐺)))
210208, 209syl6eqr 2817 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐹 = ((𝐹(𝑆𝐺)) ∘ (𝑆𝐺)))
2116, 35ltrncom 36626 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑆𝐺) ∈ 𝑇 ∧ (𝐹(𝑆𝐺)) ∈ 𝑇) → ((𝑆𝐺) ∘ (𝐹(𝑆𝐺))) = ((𝐹(𝑆𝐺)) ∘ (𝑆𝐺)))
212174, 180, 183, 211syl3anc 1490 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → ((𝑆𝐺) ∘ (𝐹(𝑆𝐺))) = ((𝐹(𝑆𝐺)) ∘ (𝑆𝐺)))
213210, 212eqtr4d 2802 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐹 = ((𝑆𝐺) ∘ (𝐹(𝑆𝐺))))
214165, 173coeq12d 5455 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝑥𝑧) = ((𝑆𝐺) ∘ (𝐹(𝑆𝐺))))
215213, 214eqtr4d 2802 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝐹 = (𝑥𝑧))
216167eqcomd 2771 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → 𝑆 = 𝑦)
217215, 216jca 507 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))
218171, 199, 217jca31 510 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) → (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)))
219163, 218impbida 835 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍))) → ((((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦)) ↔ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)))
220219pm5.32da 574 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) ↔ (((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋))))
221 df-3an 1109 . . . . . 6 (((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) ↔ (((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)))
222220, 221syl6bbr 280 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦𝐺) ∧ 𝑦𝐸) ∧ ((𝑧𝑇 ∧ (𝑅𝑧) (𝑋 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥𝑧) ∧ 𝑆 = 𝑦))) ↔ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋))))
22347, 132, 2223bitrd 296 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩)) ↔ ((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋))))
2242234exbidv 2021 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (∃𝑥𝑦𝑧𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩)) ↔ ∃𝑥𝑦𝑧𝑤((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋))))
225 fvex 6388 . . . 4 (𝑆𝐺) ∈ V
226225cnvex 7311 . . . . 5 (𝑆𝐺) ∈ V
22776, 226coex 7316 . . . 4 (𝐹(𝑆𝐺)) ∈ V
22835fvexi 6389 . . . . . 6 𝑇 ∈ V
229228mptex 6679 . . . . 5 (𝑇 ↦ ( I ↾ 𝐵)) ∈ V
23043, 229eqeltri 2840 . . . 4 𝑍 ∈ V
231 biidd 253 . . . 4 (𝑥 = (𝑆𝐺) → (((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋) ↔ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)))
232 eleq1 2832 . . . . . 6 (𝑦 = 𝑆 → (𝑦𝐸𝑆𝐸))
233232anbi2d 622 . . . . 5 (𝑦 = 𝑆 → ((𝐹𝑇𝑦𝐸) ↔ (𝐹𝑇𝑆𝐸)))
234233anbi1d 623 . . . 4 (𝑦 = 𝑆 → (((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋) ↔ ((𝐹𝑇𝑆𝐸) ∧ (𝑅𝑧) 𝑋)))
235 fveq2 6375 . . . . . 6 (𝑧 = (𝐹(𝑆𝐺)) → (𝑅𝑧) = (𝑅‘(𝐹(𝑆𝐺))))
236235breq1d 4819 . . . . 5 (𝑧 = (𝐹(𝑆𝐺)) → ((𝑅𝑧) 𝑋 ↔ (𝑅‘(𝐹(𝑆𝐺))) 𝑋))
237236anbi2d 622 . . . 4 (𝑧 = (𝐹(𝑆𝐺)) → (((𝐹𝑇𝑆𝐸) ∧ (𝑅𝑧) 𝑋) ↔ ((𝐹𝑇𝑆𝐸) ∧ (𝑅‘(𝐹(𝑆𝐺))) 𝑋)))
238 biidd 253 . . . 4 (𝑤 = 𝑍 → (((𝐹𝑇𝑆𝐸) ∧ (𝑅‘(𝐹(𝑆𝐺))) 𝑋) ↔ ((𝐹𝑇𝑆𝐸) ∧ (𝑅‘(𝐹(𝑆𝐺))) 𝑋)))
239225, 77, 227, 230, 231, 234, 237, 238ceqsex4v 3400 . . 3 (∃𝑥𝑦𝑧𝑤((𝑥 = (𝑆𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹(𝑆𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹𝑇𝑦𝐸) ∧ (𝑅𝑧) 𝑋)) ↔ ((𝐹𝑇𝑆𝐸) ∧ (𝑅‘(𝐹(𝑆𝐺))) 𝑋))
240224, 239syl6bb 278 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (∃𝑥𝑦𝑧𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦+𝑧, 𝑤⟩)) ↔ ((𝐹𝑇𝑆𝐸) ∧ (𝑅‘(𝐹(𝑆𝐺))) 𝑋)))
24113, 33, 2403bitrd 296 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵 ∧ ¬ 𝑋 𝑊) ∧ ((𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ (𝑄 (𝑋 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼𝑋) ↔ ((𝐹𝑇𝑆𝐸) ∧ (𝑅‘(𝐹(𝑆𝐺))) 𝑋)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  Vcvv 3350  cop 4340   class class class wbr 4809  cmpt 4888   I cid 5184  ccnv 5276  cres 5279  ccom 5281  wf 6064  1-1-ontowf1o 6067  cfv 6068  crio 6802  (class class class)co 6842  cmpt2 6844  Basecbs 16132  +gcplusg 16216  Scalarcsca 16219  lecple 16223  occoc 16224  joincjn 17212  meetcmee 17213  Latclat 17313  LSSumclsm 18315  LSubSpclss 19201  Atomscatm 35151  HLchlt 35238  LHypclh 35872  LTrncltrn 35989  trLctrl 36046  TEndoctendo 36640  DVecHcdvh 36966  DIsoBcdib 37026  DIsoCcdic 37060  DIsoHcdih 37116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-riotaBAD 34841
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-tpos 7555  df-undef 7602  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-sets 16139  df-ress 16140  df-plusg 16229  df-mulr 16230  df-sca 16232  df-vsca 16233  df-0g 16370  df-proset 17196  df-poset 17214  df-plt 17226  df-lub 17242  df-glb 17243  df-join 17244  df-meet 17245  df-p0 17307  df-p1 17308  df-lat 17314  df-clat 17376  df-mgm 17510  df-sgrp 17552  df-mnd 17563  df-submnd 17604  df-grp 17694  df-minusg 17695  df-sbg 17696  df-subg 17857  df-cntz 18015  df-lsm 18317  df-cmn 18461  df-abl 18462  df-mgp 18757  df-ur 18769  df-ring 18816  df-oppr 18890  df-dvdsr 18908  df-unit 18909  df-invr 18939  df-dvr 18950  df-drng 19018  df-lmod 19134  df-lss 19202  df-lsp 19244  df-lvec 19375  df-oposet 35064  df-ol 35066  df-oml 35067  df-covers 35154  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-llines 35386  df-lplanes 35387  df-lvols 35388  df-lines 35389  df-psubsp 35391  df-pmap 35392  df-padd 35684  df-lhyp 35876  df-laut 35877  df-ldil 35992  df-ltrn 35993  df-trl 36047  df-tendo 36643  df-edring 36645  df-disoa 36917  df-dvech 36967  df-dib 37027  df-dic 37061  df-dih 37117
This theorem is referenced by:  dihopelvalc  37137
  Copyright terms: Public domain W3C validator