dihopelvalcpre - Mathbox for Norm Megill

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

Theorem dihopelvalcpre 36537

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.

Step	Hyp	Ref	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‘𝑈)
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11	dihvalcq 36525	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))))
13	12	eleq2d 2687	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊)))))
14		simp1 1061	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
15		simp3l 1089	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
16		dihopelvalcp.v	. . . . 5 ⊢ 𝑉 = (LSubSp‘𝑈)
17	2, 5, 6, 10, 9, 16	diclss 36482	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐶‘𝑄) ∈ 𝑉)
18	14, 15, 17	syl2anc 693	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐶‘𝑄) ∈ 𝑉)
19		simp1l 1085	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
20		hllat 34650	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
21	19, 20	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
22		simp2l 1087	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
23		simp1r 1086	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
24	1, 6	lhpbase 35284	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
25	23, 24	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
26	1, 4	latmcl 17052	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
27	21, 22, 25, 26	syl3anc 1326	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
28	1, 2, 4	latmle2 17077	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊)
29	21, 22, 25, 28	syl3anc 1326	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ≤ 𝑊)
30	1, 2, 6, 10, 8, 16	diblss 36459	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
31	14, 27, 29, 30	syl12anc 1324	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
32		dihopelvalcp.d	. . . 4 ⊢ + = (+_g‘𝑈)
33	6, 10, 32, 16, 11	dvhopellsm 36406	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶‘𝑄) ∈ 𝑉 ∧ (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
34	14, 18, 31, 33	syl3anc 1326	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
35		dihopelvalcp.p	. . . . . . . . 9 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
36		dihopelvalcp.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
37		dihopelvalcp.e	. . . . . . . . 9 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
38		dihopelvalcp.g	. . . . . . . . 9 ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
39		vex 3203	. . . . . . . . 9 ⊢ 𝑥 ∈ V
40		vex 3203	. . . . . . . . 9 ⊢ 𝑦 ∈ V
41	2, 5, 6, 35, 36, 37, 9, 38, 39, 40	dicopelval2 36470	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
42	14, 15, 41	syl2anc 693	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
43		dihopelvalcp.r	. . . . . . . . 9 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
44		dihopelvalcp.z	. . . . . . . . 9 ⊢ 𝑍 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
45	1, 2, 6, 36, 43, 44, 8	dibopelval3 36437	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
46	14, 27, 29, 45	syl12anc 1324	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
47	42, 46	anbi12d 747	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))))
48	47	anbi1d 741	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
49		simpl1 1064	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
50		simprll 802	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑦‘𝐺))
51		simprlr 803	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑦 ∈ 𝐸)
52	2, 5, 6, 35	lhpocnel2 35305	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53	49, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
54		simpl3l 1116	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
55	2, 5, 6, 36, 38	ltrniotacl 35867	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
56	49, 53, 54, 55	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝐺 ∈ 𝑇)
57	6, 36, 37	tendocl 36055	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑦‘𝐺) ∈ 𝑇)
58	49, 51, 56, 57	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦‘𝐺) ∈ 𝑇)
59	50, 58	eqeltrd 2701	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 ∈ 𝑇)
60		simprll 802	. . . . . . . . . . . 12 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → 𝑧 ∈ 𝑇)
61	60	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑧 ∈ 𝑇)
62		simprrr 805	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
63	1, 6, 36, 37, 44	tendo0cl 36078	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑍 ∈ 𝐸)
64	49, 63	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑍 ∈ 𝐸)
65	62, 64	eqeltrd 2701	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 ∈ 𝐸)
66		eqid 2622	. . . . . . . . . . . 12 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
67		eqid 2622	. . . . . . . . . . . 12 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
68	6, 36, 37, 10, 66, 32, 67	dvhopvadd 36382	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑧 ∈ 𝑇 ∧ 𝑤 ∈ 𝐸)) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
69	49, 59, 51, 61, 65, 68	syl122anc 1335	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
70		dihopelvalcp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑎‘ℎ) ∘ (𝑏‘ℎ))))
71	6, 36, 37, 10, 66, 70, 67	dvhfplusr 36373	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+_g‘(Scalar‘𝑈)) = 𝑂)
72	49, 71	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (+_g‘(Scalar‘𝑈)) = 𝑂)
73	72	oveqd 6667	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦(+_g‘(Scalar‘𝑈))𝑤) = (𝑦𝑂𝑤))
74	73	opeq2d 4409	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
75	69, 74	eqtrd 2656	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
76	75	eqeq2d 2632	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩))
77		dihopelvalcp.f	. . . . . . . . . 10 ⊢ 𝐹 ∈ V
78		dihopelvalcp.s	. . . . . . . . . 10 ⊢ 𝑆 ∈ V
79	77, 78	opth 4945	. . . . . . . . 9 ⊢ (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)))
80	62	oveq2d 6666	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = (𝑦𝑂𝑍))
81	1, 6, 36, 37, 44, 70	tendo0plr 36080	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸) → (𝑦𝑂𝑍) = 𝑦)
82	49, 51, 81	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑍) = 𝑦)
83	80, 82	eqtrd 2656	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = 𝑦)
84	83	eqeq2d 2632	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑆 = (𝑦𝑂𝑤) ↔ 𝑆 = 𝑦))
85	84	anbi2d 740	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ((𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
86	79, 85	syl5bb 272	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
87	76, 86	bitrd 268	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
88	87	pm5.32da 673	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))))
89		simplll 798	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑥 = (𝑦‘𝐺))
90	89	adantl 482	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
91		simprrr 805	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 = 𝑦)
92	91	fveq1d 6193	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) = (𝑦‘𝐺))
93	90, 92	eqtr4d 2659	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑆‘𝐺))
94	91	eqcomd 2628	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 = 𝑆)
95		coass 5654	. . . . . . . . . . 11 ⊢ ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧))
96		simpl1 1064	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
97		simpllr 799	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑦 ∈ 𝐸)
98	97	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
99	91, 98	eqeltrd 2701	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 ∈ 𝐸)
100	56	adantrr 753	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
101	6, 36, 37	tendocl 36055	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑆‘𝐺) ∈ 𝑇)
102	96, 99, 100, 101	syl3anc 1326	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) ∈ 𝑇)
103	1, 6, 36	ltrn1o 35410	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
104	96, 102, 103	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
105		f1ococnv1 6165	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐺):𝐵–1-1-onto→𝐵 → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
106	104, 105	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
107	106	coeq1d 5283	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (( I ↾ 𝐵) ∘ 𝑧))
108	60	ad2antrl 764	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
109	1, 6, 36	ltrn1o 35410	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → 𝑧:𝐵–1-1-onto→𝐵)
110	96, 108, 109	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧:𝐵–1-1-onto→𝐵)
111		f1of 6137	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵–1-1-onto→𝐵 → 𝑧:𝐵⟶𝐵)
112		fcoi2 6079	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
113	110, 111, 112	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
114	107, 113	eqtr2d 2657	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧))
115		simprrl 804	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
116	93	coeq1d 5283	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ 𝑧))
117	115, 116	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = ((𝑆‘𝐺) ∘ 𝑧))
118	117	coeq1d 5283	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
119	6, 36	ltrncnv 35432	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → ^◡(𝑆‘𝐺) ∈ 𝑇)
120	96, 102, 119	syl2anc 693	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ^◡(𝑆‘𝐺) ∈ 𝑇)
121	6, 36	ltrnco 36007	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
122	96, 102, 108, 121	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
123	6, 36	ltrncom 36026	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡(𝑆‘𝐺) ∈ 𝑇 ∧ ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
124	96, 120, 122, 123	syl3anc 1326	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
125	118, 124	eqtr4d 2659	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)))
126	95, 114, 125	3eqtr4a 2682	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
127		simplrr 801	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑤 = 𝑍)
128	127	adantl 482	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑤 = 𝑍)
129	126, 128	jca 554	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))
130	93, 94, 129	jca31 557	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)))
131	130	ex 450	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))))
132	131	pm4.71rd 667	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
133	88, 132	bitrd 268	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
134		simprrl 804	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
135		simpll1 1100	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
136	89	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
137	97	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
138	135, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
139		simpl3l 1116	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
140	139	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
141	135, 138, 140, 55	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
142	135, 137, 141, 57	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑦‘𝐺) ∈ 𝑇)
143	136, 142	eqeltrd 2701	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 ∈ 𝑇)
144	60	ad2antrl 764	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
145	6, 36	ltrnco 36007	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (𝑥 ∘ 𝑧) ∈ 𝑇)
146	135, 143, 144, 145	syl3anc 1326	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) ∈ 𝑇)
147	134, 146	eqeltrd 2701	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 ∈ 𝑇)
148		simpl1l 1112	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝐾 ∈ HL)
149	148	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ HL)
150	149, 20	syl 17	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ Lat)
151	1, 6, 36, 43	trlcl 35451	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ∈ 𝐵)
152	135, 144, 151	syl2anc 693	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ∈ 𝐵)
153		simpl2l 1114	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑋 ∈ 𝐵)
154	153	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑋 ∈ 𝐵)
155		simpl1r 1113	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑊 ∈ 𝐻)
156	155	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐻)
157	156, 24	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐵)
158	150, 154, 157, 26	syl3anc 1326	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ∈ 𝐵)
159		simprlr 803	. . . . . . . . . . 11 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
160	159	ad2antrl 764	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
161	1, 2, 4	latmle1 17076	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑋)
162	150, 154, 157, 161	syl3anc 1326	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ≤ 𝑋)
163	1, 2, 150, 152, 158, 154, 160, 162	lattrd 17058	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ 𝑋)
164	147, 137, 163	jca31 557	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))
165		simprll 802	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑆‘𝐺))
166	165	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑆‘𝐺))
167		simprlr 803	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑦 = 𝑆)
168	167	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 = 𝑆)
169	168	fveq1d 6193	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑦‘𝐺) = (𝑆‘𝐺))
170	166, 169	eqtr4d 2659	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑦‘𝐺))
171		simprlr 803	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 ∈ 𝐸)
172	170, 171	jca 554	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸))
173		simprrl 804	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
174	173	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
175		simpll1 1100	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
176		simprll 802	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 ∈ 𝑇)
177	168, 171	eqeltrrd 2702	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 ∈ 𝐸)
178	175, 52	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
179	139	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
180	175, 178, 179, 55	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐺 ∈ 𝑇)
181	175, 177, 180, 101	syl3anc 1326	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺) ∈ 𝑇)
182	175, 181, 119	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ^◡(𝑆‘𝐺) ∈ 𝑇)
183	6, 36	ltrnco 36007	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ^◡(𝑆‘𝐺) ∈ 𝑇) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
184	175, 176, 182, 183	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
185	174, 184	eqeltrd 2701	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 ∈ 𝑇)
186		simprr 796	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑋)
187	2, 6, 36, 43	trlle 35471	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ≤ 𝑊)
188	175, 185, 187	syl2anc 693	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑊)
189	148	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ HL)
190	189, 20	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ Lat)
191	175, 185, 151	syl2anc 693	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ∈ 𝐵)
192	153	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑋 ∈ 𝐵)
193	155	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐻)
194	193, 24	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐵)
195	1, 2, 4	latlem12 17078	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝑧) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
196	190, 191, 192, 194, 195	syl13anc 1328	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
197	186, 188, 196	mpbi2and 956	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
198		simprrr 805	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
199	198	adantr 481	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑤 = 𝑍)
200	185, 197, 199	jca31 557	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))
201	175, 181, 103	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
202	201, 105	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
203	202	coeq2d 5284	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))) = (𝐹 ∘ ( I ↾ 𝐵)))
204	1, 6, 36	ltrn1o 35410	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
205	175, 176, 204	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹:𝐵–1-1-onto→𝐵)
206		f1of 6137	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹:𝐵⟶𝐵)
207		fcoi1 6078	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
208	205, 206, 207	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
209	203, 208	eqtr2d 2657	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))))
210		coass 5654	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)) = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)))
211	209, 210	syl6eqr 2674	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
212	6, 36	ltrncom 36026	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
213	175, 181, 184, 212	syl3anc 1326	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
214	211, 213	eqtr4d 2659	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
215	166, 174	coeq12d 5286	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
216	214, 215	eqtr4d 2659	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝑥 ∘ 𝑧))
217	168	eqcomd 2628	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 = 𝑦)
218	216, 217	jca 554	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))
219	172, 200, 218	jca31 557	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
220	164, 219	impbida 877	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
221	220	pm5.32da 673	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
222		df-3an 1039	. . . . . 6 ⊢ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
223	221, 222	syl6bbr 278	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
224	48, 133, 223	3bitrd 294	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
225	224	4exbidv 1854	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
226		fvex 6201	. . . 4 ⊢ (𝑆‘𝐺) ∈ V
227	226	cnvex 7113	. . . . 5 ⊢ ^◡(𝑆‘𝐺) ∈ V
228	77, 227	coex 7118	. . . 4 ⊢ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ V
229		fvex 6201	. . . . . . 7 ⊢ ((LTrn‘𝐾)‘𝑊) ∈ V
230	36, 229	eqeltri 2697	. . . . . 6 ⊢ 𝑇 ∈ V
231	230	mptex 6486	. . . . 5 ⊢ (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V
232	44, 231	eqeltri 2697	. . . 4 ⊢ 𝑍 ∈ V
233		biidd 252	. . . 4 ⊢ (𝑥 = (𝑆‘𝐺) → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
234		eleq1 2689	. . . . . 6 ⊢ (𝑦 = 𝑆 → (𝑦 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸))
235	234	anbi2d 740	. . . . 5 ⊢ (𝑦 = 𝑆 → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ↔ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)))
236	235	anbi1d 741	. . . 4 ⊢ (𝑦 = 𝑆 → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
237		fveq2 6191	. . . . . 6 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (𝑅‘𝑧) = (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))))
238	237	breq1d 4663	. . . . 5 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → ((𝑅‘𝑧) ≤ 𝑋 ↔ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
239	238	anbi2d 740	. . . 4 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
240		biidd 252	. . . 4 ⊢ (𝑤 = 𝑍 → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
241	226, 78, 228, 232, 233, 236, 239, 240	ceqsex4v 3247	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
242	225, 241	syl6bb 276	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
243	13, 34, 242	3bitrd 294	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 Vcvv 3200 ⟨cop 4183 class class class wbr 4653 ↦ cmpt 4729 I cid 5023 ^◡ccnv 5113 ↾ cres 5116 ∘ ccom 5118 ⟶wf 5884 –1-1-onto→wf1o 5887 ‘cfv 5888 ℩crio 6610 (class class class)co 6650 ↦ cmpt2 6652 Basecbs 15857 +_gcplusg 15941 Scalarcsca 15944 lecple 15948 occoc 15949 joincjn 16944 meetcmee 16945 Latclat 17045 LSSumclsm 18049 LSubSpclss 18932 Atomscatm 34550 HLchlt 34637 LHypclh 35270 LTrncltrn 35387 trLctrl 35445 TEndoctendo 36040 DVecHcdvh 36367 DIsoBcdib 36427 DIsoCcdic 36461 DIsoHcdih 36517

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-riotaBAD 34239

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-iin 4523 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-tpos 7352 df-undef 7399 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-n0 11293 df-z 11378 df-uz 11688 df-fz 12327 df-struct 15859 df-ndx 15860 df-slot 15861 df-base 15863 df-sets 15864 df-ress 15865 df-plusg 15954 df-mulr 15955 df-sca 15957 df-vsca 15958 df-0g 16102 df-preset 16928 df-poset 16946 df-plt 16958 df-lub 16974 df-glb 16975 df-join 16976 df-meet 16977 df-p0 17039 df-p1 17040 df-lat 17046 df-clat 17108 df-mgm 17242 df-sgrp 17284 df-mnd 17295 df-submnd 17336 df-grp 17425 df-minusg 17426 df-sbg 17427 df-subg 17591 df-cntz 17750 df-lsm 18051 df-cmn 18195 df-abl 18196 df-mgp 18490 df-ur 18502 df-ring 18549 df-oppr 18623 df-dvdsr 18641 df-unit 18642 df-invr 18672 df-dvr 18683 df-drng 18749 df-lmod 18865 df-lss 18933 df-lsp 18972 df-lvec 19103 df-oposet 34463 df-ol 34465 df-oml 34466 df-covers 34553 df-ats 34554 df-atl 34585 df-cvlat 34609 df-hlat 34638 df-llines 34784 df-lplanes 34785 df-lvols 34786 df-lines 34787 df-psubsp 34789 df-pmap 34790 df-padd 35082 df-lhyp 35274 df-laut 35275 df-ldil 35390 df-ltrn 35391 df-trl 35446 df-tendo 36043 df-edring 36045 df-disoa 36318 df-dvech 36368 df-dib 36428 df-dic 36462 df-dih 36518

This theorem is referenced by: dihopelvalc 36538

W3C validator