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 41947

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 41935	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))))
13	12	eleq2d 2855	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊)))))
14		simp1 1152	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
15		simp3l 1218	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
16		dihopelvalcp.v	. . . . 5 ⊢ 𝑉 = (LSubSp‘𝑈)
17	2, 5, 6, 10, 9, 16	diclss 41892	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐶‘𝑄) ∈ 𝑉)
18	14, 15, 17	syl2anc 595	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐶‘𝑄) ∈ 𝑉)
19		simp1l 1214	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
20	19	hllatd 40063	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
21		simp2l 1216	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
22		simp1r 1215	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
23	1, 6	lhpbase 40697	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
24	22, 23	syl 18	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
25	1, 4	latmcl 18496	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
26	20, 21, 24, 25	syl3anc 1396	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
27	1, 2, 4	latmle2 18521	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊)
28	20, 21, 24, 27	syl3anc 1396	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ≤ 𝑊)
29	1, 2, 6, 10, 8, 16	diblss 41869	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
30	14, 26, 28, 29	syl12anc 849	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
31		dihopelvalcp.d	. . . 4 ⊢ + = (+_g‘𝑈)
32	6, 10, 31, 16, 11	dvhopellsm 41816	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶‘𝑄) ∈ 𝑉 ∧ (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
33	14, 18, 30, 32	syl3anc 1396	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
34		dihopelvalcp.p	. . . . . . . . 9 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
35		dihopelvalcp.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
36		dihopelvalcp.e	. . . . . . . . 9 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
37		dihopelvalcp.g	. . . . . . . . 9 ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
38		vex 3465	. . . . . . . . 9 ⊢ 𝑥 ∈ V
39		vex 3465	. . . . . . . . 9 ⊢ 𝑦 ∈ V
40	2, 5, 6, 34, 35, 36, 9, 37, 38, 39	dicopelval2 41880	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
41	14, 15, 40	syl2anc 595	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
42		dihopelvalcp.r	. . . . . . . . 9 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
43		dihopelvalcp.z	. . . . . . . . 9 ⊢ 𝑍 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
44	1, 2, 6, 35, 42, 43, 8	dibopelval3 41847	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
45	14, 26, 28, 44	syl12anc 849	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
46	41, 45	anbi12d 643	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))))
47	46	anbi1d 642	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
48		simpl1 1208	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
49		simprll 790	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑦‘𝐺))
50		simprlr 791	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑦 ∈ 𝐸)
51	2, 5, 6, 34	lhpocnel2 40718	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
52	48, 51	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53		simpl3l 1245	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
54	2, 5, 6, 35, 37	ltrniotacl 41278	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
55	48, 52, 53, 54	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝐺 ∈ 𝑇)
56	6, 35, 36	tendocl 41466	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑦‘𝐺) ∈ 𝑇)
57	48, 50, 55, 56	syl3anc 1396	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦‘𝐺) ∈ 𝑇)
58	49, 57	eqeltrd 2869	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 ∈ 𝑇)
59		simprll 790	. . . . . . . . . . . 12 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → 𝑧 ∈ 𝑇)
60	59	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑧 ∈ 𝑇)
61		simprrr 793	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
62	1, 6, 35, 36, 43	tendo0cl 41489	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑍 ∈ 𝐸)
63	48, 62	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑍 ∈ 𝐸)
64	61, 63	eqeltrd 2869	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 ∈ 𝐸)
65		eqid 2769	. . . . . . . . . . . 12 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
66		eqid 2769	. . . . . . . . . . . 12 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
67	6, 35, 36, 10, 65, 31, 66	dvhopvadd 41792	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑧 ∈ 𝑇 ∧ 𝑤 ∈ 𝐸)) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
68	48, 58, 50, 60, 64, 67	syl122anc 1404	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
69		dihopelvalcp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑎‘ℎ) ∘ (𝑏‘ℎ))))
70	6, 35, 36, 10, 65, 69, 66	dvhfplusr 41783	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+_g‘(Scalar‘𝑈)) = 𝑂)
71	48, 70	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (+_g‘(Scalar‘𝑈)) = 𝑂)
72	71	oveqd 7428	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦(+_g‘(Scalar‘𝑈))𝑤) = (𝑦𝑂𝑤))
73	72	opeq2d 4847	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
74	68, 73	eqtrd 2804	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
75	74	eqeq2d 2780	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩))
76		dihopelvalcp.f	. . . . . . . . . 10 ⊢ 𝐹 ∈ V
77		dihopelvalcp.s	. . . . . . . . . 10 ⊢ 𝑆 ∈ V
78	76, 77	opth 5459	. . . . . . . . 9 ⊢ (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)))
79	61	oveq2d 7427	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = (𝑦𝑂𝑍))
80	1, 6, 35, 36, 43, 69	tendo0plr 41491	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸) → (𝑦𝑂𝑍) = 𝑦)
81	48, 50, 80	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑍) = 𝑦)
82	79, 81	eqtrd 2804	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = 𝑦)
83	82	eqeq2d 2780	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑆 = (𝑦𝑂𝑤) ↔ 𝑆 = 𝑦))
84	83	anbi2d 641	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ((𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
85	78, 84	bitrid 286	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
86	75, 85	bitrd 282	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
87	86	pm5.32da 589	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))))
88		simplll 786	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑥 = (𝑦‘𝐺))
89	88	adantl 486	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
90		simprrr 793	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 = 𝑦)
91	90	fveq1d 6884	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) = (𝑦‘𝐺))
92	89, 91	eqtr4d 2807	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑆‘𝐺))
93	90	eqcomd 2775	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 = 𝑆)
94		coass 6268	. . . . . . . . . . 11 ⊢ ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧))
95		simpl1 1208	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
96		simpllr 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑦 ∈ 𝐸)
97	96	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
98	90, 97	eqeltrd 2869	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 ∈ 𝐸)
99	55	adantrr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
100	6, 35, 36	tendocl 41466	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑆‘𝐺) ∈ 𝑇)
101	95, 98, 99, 100	syl3anc 1396	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) ∈ 𝑇)
102	1, 6, 35	ltrn1o 40823	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
103	95, 101, 102	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
104		f1ococnv1 6851	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐺):𝐵–1-1-onto→𝐵 → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
105	103, 104	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
106	105	coeq1d 5848	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (( I ↾ 𝐵) ∘ 𝑧))
107	59	ad2antrl 740	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
108	1, 6, 35	ltrn1o 40823	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → 𝑧:𝐵–1-1-onto→𝐵)
109	95, 107, 108	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧:𝐵–1-1-onto→𝐵)
110		f1of 6821	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵–1-1-onto→𝐵 → 𝑧:𝐵⟶𝐵)
111		fcoi2 6754	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
112	109, 110, 111	3syl 19	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
113	106, 112	eqtr2d 2805	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧))
114		simprrl 792	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
115	92	coeq1d 5848	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ 𝑧))
116	114, 115	eqtrd 2804	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = ((𝑆‘𝐺) ∘ 𝑧))
117	116	coeq1d 5848	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
118	6, 35	ltrncnv 40845	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → ^◡(𝑆‘𝐺) ∈ 𝑇)
119	95, 101, 118	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ^◡(𝑆‘𝐺) ∈ 𝑇)
120	6, 35	ltrnco 41418	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
121	95, 101, 107, 120	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
122	6, 35	ltrncom 41437	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡(𝑆‘𝐺) ∈ 𝑇 ∧ ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
123	95, 119, 121, 122	syl3anc 1396	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
124	117, 123	eqtr4d 2807	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)))
125	94, 113, 124	3eqtr4a 2830	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
126		simplrr 789	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑤 = 𝑍)
127	126	adantl 486	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑤 = 𝑍)
128	125, 127	jca 520	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))
129	92, 93, 128	jca31 523	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)))
130	129	ex 417	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))))
131	130	pm4.71rd 571	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
132	87, 131	bitrd 282	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
133		simprrl 792	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
134		simpll1 1229	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
135	88	adantl 486	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
136	96	adantl 486	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
137	134, 51	syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
138		simpl3l 1245	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
139	138	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
140	134, 137, 139, 54	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
141	134, 136, 140, 56	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑦‘𝐺) ∈ 𝑇)
142	135, 141	eqeltrd 2869	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 ∈ 𝑇)
143	59	ad2antrl 740	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
144	6, 35	ltrnco 41418	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (𝑥 ∘ 𝑧) ∈ 𝑇)
145	134, 142, 143, 144	syl3anc 1396	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) ∈ 𝑇)
146	133, 145	eqeltrd 2869	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 ∈ 𝑇)
147		simpl1l 1241	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝐾 ∈ HL)
148	147	adantr 485	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ HL)
149	148	hllatd 40063	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ Lat)
150	1, 6, 35, 42	trlcl 40863	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ∈ 𝐵)
151	134, 143, 150	syl2anc 595	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ∈ 𝐵)
152		simpl2l 1243	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑋 ∈ 𝐵)
153	152	adantr 485	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑋 ∈ 𝐵)
154		simpl1r 1242	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑊 ∈ 𝐻)
155	154	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐻)
156	155, 23	syl 18	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐵)
157	149, 153, 156, 25	syl3anc 1396	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ∈ 𝐵)
158		simprlr 791	. . . . . . . . . . 11 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
159	158	ad2antrl 740	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
160	1, 2, 4	latmle1 18520	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑋)
161	149, 153, 156, 160	syl3anc 1396	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ≤ 𝑋)
162	1, 2, 149, 151, 157, 153, 159, 161	lattrd 18502	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ 𝑋)
163	146, 136, 162	jca31 523	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))
164		simprll 790	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑆‘𝐺))
165	164	adantr 485	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑆‘𝐺))
166		simprlr 791	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑦 = 𝑆)
167	166	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 = 𝑆)
168	167	fveq1d 6884	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑦‘𝐺) = (𝑆‘𝐺))
169	165, 168	eqtr4d 2807	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑦‘𝐺))
170		simprlr 791	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 ∈ 𝐸)
171	169, 170	jca 520	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸))
172		simprrl 792	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
173	172	adantr 485	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
174		simpll1 1229	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
175		simprll 790	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 ∈ 𝑇)
176	167, 170	eqeltrrd 2870	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 ∈ 𝐸)
177	174, 51	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
178	138	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
179	174, 177, 178, 54	syl3anc 1396	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐺 ∈ 𝑇)
180	174, 176, 179, 100	syl3anc 1396	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺) ∈ 𝑇)
181	174, 180, 118	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ^◡(𝑆‘𝐺) ∈ 𝑇)
182	6, 35	ltrnco 41418	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ^◡(𝑆‘𝐺) ∈ 𝑇) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
183	174, 175, 181, 182	syl3anc 1396	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
184	173, 183	eqeltrd 2869	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 ∈ 𝑇)
185		simprr 784	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑋)
186	2, 6, 35, 42	trlle 40883	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ≤ 𝑊)
187	174, 184, 186	syl2anc 595	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑊)
188	147	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ HL)
189	188	hllatd 40063	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ Lat)
190	174, 184, 150	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ∈ 𝐵)
191	152	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑋 ∈ 𝐵)
192	154	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐻)
193	192, 23	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐵)
194	1, 2, 4	latlem12 18522	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝑧) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
195	189, 190, 191, 193, 194	syl13anc 1397	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
196	185, 187, 195	mpbi2and 724	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
197		simprrr 793	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
198	197	adantr 485	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑤 = 𝑍)
199	184, 196, 198	jca31 523	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))
200	174, 180, 102	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
201	200, 104	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
202	201	coeq2d 5849	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))) = (𝐹 ∘ ( I ↾ 𝐵)))
203	1, 6, 35	ltrn1o 40823	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
204	174, 175, 203	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹:𝐵–1-1-onto→𝐵)
205		f1of 6821	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹:𝐵⟶𝐵)
206		fcoi1 6753	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
207	204, 205, 206	3syl 19	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
208	202, 207	eqtr2d 2805	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))))
209		coass 6268	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)) = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)))
210	208, 209	eqtr4di 2822	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
211	6, 35	ltrncom 41437	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
212	174, 180, 183, 211	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
213	210, 212	eqtr4d 2807	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
214	165, 173	coeq12d 5851	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
215	213, 214	eqtr4d 2807	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝑥 ∘ 𝑧))
216	167	eqcomd 2775	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 = 𝑦)
217	215, 216	jca 520	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))
218	171, 199, 217	jca31 523	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
219	163, 218	impbida 812	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
220	219	pm5.32da 589	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
221		df-3an 1103	. . . . . 6 ⊢ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
222	220, 221	bitr4di 292	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
223	47, 132, 222	3bitrd 308	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
224	223	4exbidv 1953	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
225		fvex 6895	. . . 4 ⊢ (𝑆‘𝐺) ∈ V
226	225	cnvex 7922	. . . . 5 ⊢ ^◡(𝑆‘𝐺) ∈ V
227	76, 226	coex 7927	. . . 4 ⊢ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ V
228	35	fvexi 6896	. . . . . 6 ⊢ 𝑇 ∈ V
229	228	mptex 7222	. . . . 5 ⊢ (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V
230	43, 229	eqeltri 2865	. . . 4 ⊢ 𝑍 ∈ V
231		biidd 265	. . . 4 ⊢ (𝑥 = (𝑆‘𝐺) → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
232		eleq1 2857	. . . . . 6 ⊢ (𝑦 = 𝑆 → (𝑦 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸))
233	232	anbi2d 641	. . . . 5 ⊢ (𝑦 = 𝑆 → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ↔ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)))
234	233	anbi1d 642	. . . 4 ⊢ (𝑦 = 𝑆 → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
235		fveq2 6882	. . . . . 6 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (𝑅‘𝑧) = (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))))
236	235	breq1d 5121	. . . . 5 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → ((𝑅‘𝑧) ≤ 𝑋 ↔ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
237	236	anbi2d 641	. . . 4 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
238		biidd 265	. . . 4 ⊢ (𝑤 = 𝑍 → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
239	225, 77, 227, 230, 231, 234, 237, 238	ceqsex4v 3514	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
240	224, 239	bitrdi 290	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
241	13, 33, 240	3bitrd 308	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∃wex 1806 ∈ wcel 2149 Vcvv 3461 ⟨cop 4598 class class class wbr 5111 ↦ cmpt 5194 I cid 5556 ^◡ccnv 5661 ↾ cres 5664 ∘ ccom 5666 ⟶wf 6533 –1-1-onto→wf1o 6536 ‘cfv 6537 ℩crio 7367 (class class class)co 7411 ∈ cmpo 7413 Basecbs 17269 +_gcplusg 17310 Scalarcsca 17313 lecple 17317 occoc 17318 joincjn 18367 meetcmee 18368 Latclat 18487 LSSumclsm 19704 LSubSpclss 21030 Atomscatm 39962 HLchlt 40049 LHypclh 40683 LTrncltrn 40800 trLctrl 40857 TEndoctendo 41451 DVecHcdvh 41777 DIsoBcdib 41837 DIsoCcdic 41871 DIsoHcdih 41927

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-riotaBAD 39652

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-tpos 8222 df-undef 8269 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-n0 12505 df-z 12592 df-uz 12863 df-fz 13536 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-sca 17326 df-vsca 17327 df-0g 17494 df-proset 18350 df-poset 18369 df-plt 18384 df-lub 18400 df-glb 18401 df-join 18402 df-meet 18403 df-p0 18479 df-p1 18480 df-lat 18488 df-clat 18555 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-submnd 18842 df-grp 19003 df-minusg 19004 df-sbg 19005 df-subg 19189 df-cntz 19387 df-lsm 19706 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-drng 20815 df-lmod 20961 df-lss 21031 df-lsp 21071 df-lvec 21202 df-oposet 39875 df-ol 39877 df-oml 39878 df-covers 39965 df-ats 39966 df-atl 39997 df-cvlat 40021 df-hlat 40050 df-llines 40197 df-lplanes 40198 df-lvols 40199 df-lines 40200 df-psubsp 40202 df-pmap 40203 df-padd 40495 df-lhyp 40687 df-laut 40688 df-ldil 40803 df-ltrn 40804 df-trl 40858 df-tendo 41454 df-edring 41456 df-disoa 41728 df-dvech 41778 df-dib 41838 df-dic 41872 df-dih 41928

This theorem is referenced by: dihopelvalc 41948

W3C validator