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 39269

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 39257	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))))
13	12	eleq2d 2825	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊)))))
14		simp1 1135	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
15		simp3l 1200	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
16		dihopelvalcp.v	. . . . 5 ⊢ 𝑉 = (LSubSp‘𝑈)
17	2, 5, 6, 10, 9, 16	diclss 39214	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐶‘𝑄) ∈ 𝑉)
18	14, 15, 17	syl2anc 584	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐶‘𝑄) ∈ 𝑉)
19		simp1l 1196	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
20	19	hllatd 37385	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
21		simp2l 1198	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
22		simp1r 1197	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
23	1, 6	lhpbase 38019	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
24	22, 23	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
25	1, 4	latmcl 18167	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
26	20, 21, 24, 25	syl3anc 1370	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
27	1, 2, 4	latmle2 18192	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊)
28	20, 21, 24, 27	syl3anc 1370	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ≤ 𝑊)
29	1, 2, 6, 10, 8, 16	diblss 39191	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
30	14, 26, 28, 29	syl12anc 834	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
31		dihopelvalcp.d	. . . 4 ⊢ + = (+_g‘𝑈)
32	6, 10, 31, 16, 11	dvhopellsm 39138	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶‘𝑄) ∈ 𝑉 ∧ (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
33	14, 18, 30, 32	syl3anc 1370	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
34		dihopelvalcp.p	. . . . . . . . 9 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
35		dihopelvalcp.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
36		dihopelvalcp.e	. . . . . . . . 9 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
37		dihopelvalcp.g	. . . . . . . . 9 ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
38		vex 3437	. . . . . . . . 9 ⊢ 𝑥 ∈ V
39		vex 3437	. . . . . . . . 9 ⊢ 𝑦 ∈ V
40	2, 5, 6, 34, 35, 36, 9, 37, 38, 39	dicopelval2 39202	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
41	14, 15, 40	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
42		dihopelvalcp.r	. . . . . . . . 9 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
43		dihopelvalcp.z	. . . . . . . . 9 ⊢ 𝑍 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
44	1, 2, 6, 35, 42, 43, 8	dibopelval3 39169	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
45	14, 26, 28, 44	syl12anc 834	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
46	41, 45	anbi12d 631	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))))
47	46	anbi1d 630	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
48		simpl1 1190	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
49		simprll 776	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑦‘𝐺))
50		simprlr 777	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑦 ∈ 𝐸)
51	2, 5, 6, 34	lhpocnel2 38040	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
52	48, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53		simpl3l 1227	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
54	2, 5, 6, 35, 37	ltrniotacl 38600	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
55	48, 52, 53, 54	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝐺 ∈ 𝑇)
56	6, 35, 36	tendocl 38788	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑦‘𝐺) ∈ 𝑇)
57	48, 50, 55, 56	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦‘𝐺) ∈ 𝑇)
58	49, 57	eqeltrd 2840	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 ∈ 𝑇)
59		simprll 776	. . . . . . . . . . . 12 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → 𝑧 ∈ 𝑇)
60	59	adantl 482	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑧 ∈ 𝑇)
61		simprrr 779	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
62	1, 6, 35, 36, 43	tendo0cl 38811	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑍 ∈ 𝐸)
63	48, 62	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑍 ∈ 𝐸)
64	61, 63	eqeltrd 2840	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 ∈ 𝐸)
65		eqid 2739	. . . . . . . . . . . 12 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
66		eqid 2739	. . . . . . . . . . . 12 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
67	6, 35, 36, 10, 65, 31, 66	dvhopvadd 39114	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑧 ∈ 𝑇 ∧ 𝑤 ∈ 𝐸)) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
68	48, 58, 50, 60, 64, 67	syl122anc 1378	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
69		dihopelvalcp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑎‘ℎ) ∘ (𝑏‘ℎ))))
70	6, 35, 36, 10, 65, 69, 66	dvhfplusr 39105	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+_g‘(Scalar‘𝑈)) = 𝑂)
71	48, 70	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (+_g‘(Scalar‘𝑈)) = 𝑂)
72	71	oveqd 7301	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦(+_g‘(Scalar‘𝑈))𝑤) = (𝑦𝑂𝑤))
73	72	opeq2d 4812	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
74	68, 73	eqtrd 2779	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
75	74	eqeq2d 2750	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩))
76		dihopelvalcp.f	. . . . . . . . . 10 ⊢ 𝐹 ∈ V
77		dihopelvalcp.s	. . . . . . . . . 10 ⊢ 𝑆 ∈ V
78	76, 77	opth 5392	. . . . . . . . 9 ⊢ (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)))
79	61	oveq2d 7300	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = (𝑦𝑂𝑍))
80	1, 6, 35, 36, 43, 69	tendo0plr 38813	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸) → (𝑦𝑂𝑍) = 𝑦)
81	48, 50, 80	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑍) = 𝑦)
82	79, 81	eqtrd 2779	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = 𝑦)
83	82	eqeq2d 2750	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑆 = (𝑦𝑂𝑤) ↔ 𝑆 = 𝑦))
84	83	anbi2d 629	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ((𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
85	78, 84	syl5bb 283	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
86	75, 85	bitrd 278	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
87	86	pm5.32da 579	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))))
88		simplll 772	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑥 = (𝑦‘𝐺))
89	88	adantl 482	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
90		simprrr 779	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 = 𝑦)
91	90	fveq1d 6785	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) = (𝑦‘𝐺))
92	89, 91	eqtr4d 2782	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑆‘𝐺))
93	90	eqcomd 2745	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 = 𝑆)
94		coass 6173	. . . . . . . . . . 11 ⊢ ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧))
95		simpl1 1190	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
96		simpllr 773	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑦 ∈ 𝐸)
97	96	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
98	90, 97	eqeltrd 2840	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 ∈ 𝐸)
99	55	adantrr 714	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
100	6, 35, 36	tendocl 38788	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑆‘𝐺) ∈ 𝑇)
101	95, 98, 99, 100	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) ∈ 𝑇)
102	1, 6, 35	ltrn1o 38145	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
103	95, 101, 102	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
104		f1ococnv1 6754	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐺):𝐵–1-1-onto→𝐵 → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
106	105	coeq1d 5773	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (( I ↾ 𝐵) ∘ 𝑧))
107	59	ad2antrl 725	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
108	1, 6, 35	ltrn1o 38145	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → 𝑧:𝐵–1-1-onto→𝐵)
109	95, 107, 108	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧:𝐵–1-1-onto→𝐵)
110		f1of 6725	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵–1-1-onto→𝐵 → 𝑧:𝐵⟶𝐵)
111		fcoi2 6658	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
112	109, 110, 111	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
113	106, 112	eqtr2d 2780	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧))
114		simprrl 778	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
115	92	coeq1d 5773	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ 𝑧))
116	114, 115	eqtrd 2779	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = ((𝑆‘𝐺) ∘ 𝑧))
117	116	coeq1d 5773	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
118	6, 35	ltrncnv 38167	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → ^◡(𝑆‘𝐺) ∈ 𝑇)
119	95, 101, 118	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ^◡(𝑆‘𝐺) ∈ 𝑇)
120	6, 35	ltrnco 38740	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
121	95, 101, 107, 120	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
122	6, 35	ltrncom 38759	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡(𝑆‘𝐺) ∈ 𝑇 ∧ ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
123	95, 119, 121, 122	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
124	117, 123	eqtr4d 2782	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)))
125	94, 113, 124	3eqtr4a 2805	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
126		simplrr 775	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑤 = 𝑍)
127	126	adantl 482	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑤 = 𝑍)
128	125, 127	jca 512	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))
129	92, 93, 128	jca31 515	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)))
130	129	ex 413	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))))
131	130	pm4.71rd 563	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
132	87, 131	bitrd 278	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
133		simprrl 778	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
134		simpll1 1211	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
135	88	adantl 482	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
136	96	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
137	134, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
138		simpl3l 1227	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
139	138	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
140	134, 137, 139, 54	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
141	134, 136, 140, 56	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑦‘𝐺) ∈ 𝑇)
142	135, 141	eqeltrd 2840	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 ∈ 𝑇)
143	59	ad2antrl 725	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
144	6, 35	ltrnco 38740	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (𝑥 ∘ 𝑧) ∈ 𝑇)
145	134, 142, 143, 144	syl3anc 1370	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) ∈ 𝑇)
146	133, 145	eqeltrd 2840	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 ∈ 𝑇)
147		simpl1l 1223	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝐾 ∈ HL)
148	147	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ HL)
149	148	hllatd 37385	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ Lat)
150	1, 6, 35, 42	trlcl 38185	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ∈ 𝐵)
151	134, 143, 150	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ∈ 𝐵)
152		simpl2l 1225	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑋 ∈ 𝐵)
153	152	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑋 ∈ 𝐵)
154		simpl1r 1224	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑊 ∈ 𝐻)
155	154	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐻)
156	155, 23	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐵)
157	149, 153, 156, 25	syl3anc 1370	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ∈ 𝐵)
158		simprlr 777	. . . . . . . . . . 11 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
159	158	ad2antrl 725	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
160	1, 2, 4	latmle1 18191	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑋)
161	149, 153, 156, 160	syl3anc 1370	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ≤ 𝑋)
162	1, 2, 149, 151, 157, 153, 159, 161	lattrd 18173	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ 𝑋)
163	146, 136, 162	jca31 515	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))
164		simprll 776	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑆‘𝐺))
165	164	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑆‘𝐺))
166		simprlr 777	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑦 = 𝑆)
167	166	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 = 𝑆)
168	167	fveq1d 6785	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑦‘𝐺) = (𝑆‘𝐺))
169	165, 168	eqtr4d 2782	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑦‘𝐺))
170		simprlr 777	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 ∈ 𝐸)
171	169, 170	jca 512	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸))
172		simprrl 778	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
173	172	adantr 481	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
174		simpll1 1211	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
175		simprll 776	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 ∈ 𝑇)
176	167, 170	eqeltrrd 2841	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 ∈ 𝐸)
177	174, 51	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
178	138	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
179	174, 177, 178, 54	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐺 ∈ 𝑇)
180	174, 176, 179, 100	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺) ∈ 𝑇)
181	174, 180, 118	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ^◡(𝑆‘𝐺) ∈ 𝑇)
182	6, 35	ltrnco 38740	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ^◡(𝑆‘𝐺) ∈ 𝑇) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
183	174, 175, 181, 182	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
184	173, 183	eqeltrd 2840	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 ∈ 𝑇)
185		simprr 770	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑋)
186	2, 6, 35, 42	trlle 38205	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ≤ 𝑊)
187	174, 184, 186	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑊)
188	147	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ HL)
189	188	hllatd 37385	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ Lat)
190	174, 184, 150	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ∈ 𝐵)
191	152	adantr 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑋 ∈ 𝐵)
192	154	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐻)
193	192, 23	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐵)
194	1, 2, 4	latlem12 18193	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝑧) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
195	189, 190, 191, 193, 194	syl13anc 1371	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
196	185, 187, 195	mpbi2and 709	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
197		simprrr 779	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
198	197	adantr 481	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑤 = 𝑍)
199	184, 196, 198	jca31 515	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))
200	174, 180, 102	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
201	200, 104	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
202	201	coeq2d 5774	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))) = (𝐹 ∘ ( I ↾ 𝐵)))
203	1, 6, 35	ltrn1o 38145	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
204	174, 175, 203	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹:𝐵–1-1-onto→𝐵)
205		f1of 6725	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹:𝐵⟶𝐵)
206		fcoi1 6657	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
207	204, 205, 206	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
208	202, 207	eqtr2d 2780	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))))
209		coass 6173	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)) = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)))
210	208, 209	eqtr4di 2797	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
211	6, 35	ltrncom 38759	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
212	174, 180, 183, 211	syl3anc 1370	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
213	210, 212	eqtr4d 2782	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
214	165, 173	coeq12d 5776	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
215	213, 214	eqtr4d 2782	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝑥 ∘ 𝑧))
216	167	eqcomd 2745	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 = 𝑦)
217	215, 216	jca 512	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))
218	171, 199, 217	jca31 515	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
219	163, 218	impbida 798	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
220	219	pm5.32da 579	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
221		df-3an 1088	. . . . . 6 ⊢ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
222	220, 221	bitr4di 289	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
223	47, 132, 222	3bitrd 305	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
224	223	4exbidv 1930	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
225		fvex 6796	. . . 4 ⊢ (𝑆‘𝐺) ∈ V
226	225	cnvex 7781	. . . . 5 ⊢ ^◡(𝑆‘𝐺) ∈ V
227	76, 226	coex 7786	. . . 4 ⊢ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ V
228	35	fvexi 6797	. . . . . 6 ⊢ 𝑇 ∈ V
229	228	mptex 7108	. . . . 5 ⊢ (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V
230	43, 229	eqeltri 2836	. . . 4 ⊢ 𝑍 ∈ V
231		biidd 261	. . . 4 ⊢ (𝑥 = (𝑆‘𝐺) → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
232		eleq1 2827	. . . . . 6 ⊢ (𝑦 = 𝑆 → (𝑦 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸))
233	232	anbi2d 629	. . . . 5 ⊢ (𝑦 = 𝑆 → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ↔ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)))
234	233	anbi1d 630	. . . 4 ⊢ (𝑦 = 𝑆 → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
235		fveq2 6783	. . . . . 6 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (𝑅‘𝑧) = (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))))
236	235	breq1d 5085	. . . . 5 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → ((𝑅‘𝑧) ≤ 𝑋 ↔ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
237	236	anbi2d 629	. . . 4 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
238		biidd 261	. . . 4 ⊢ (𝑤 = 𝑍 → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
239	225, 77, 227, 230, 231, 234, 237, 238	ceqsex4v 3486	. . 3 ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
240	224, 239	bitrdi 287	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
241	13, 33, 240	3bitrd 305	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1086 = wceq 1539 ∃wex 1782 ∈ wcel 2107 Vcvv 3433 ⟨cop 4568 class class class wbr 5075 ↦ cmpt 5158 I cid 5489 ^◡ccnv 5589 ↾ cres 5592 ∘ ccom 5594 ⟶wf 6433 –1-1-onto→wf1o 6436 ‘cfv 6437 ℩crio 7240 (class class class)co 7284 ∈ cmpo 7286 Basecbs 16921 +_gcplusg 16971 Scalarcsca 16974 lecple 16978 occoc 16979 joincjn 18038 meetcmee 18039 Latclat 18158 LSSumclsm 19248 LSubSpclss 20202 Atomscatm 37284 HLchlt 37371 LHypclh 38005 LTrncltrn 38122 trLctrl 38179 TEndoctendo 38773 DVecHcdvh 39099 DIsoBcdib 39159 DIsoCcdic 39193 DIsoHcdih 39249

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-riotaBAD 36974

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-iin 4928 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-1st 7840 df-2nd 7841 df-tpos 8051 df-undef 8098 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-map 8626 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-nn 11983 df-2 12045 df-3 12046 df-4 12047 df-5 12048 df-6 12049 df-n0 12243 df-z 12329 df-uz 12592 df-fz 13249 df-struct 16857 df-sets 16874 df-slot 16892 df-ndx 16904 df-base 16922 df-ress 16951 df-plusg 16984 df-mulr 16985 df-sca 16987 df-vsca 16988 df-0g 17161 df-proset 18022 df-poset 18040 df-plt 18057 df-lub 18073 df-glb 18074 df-join 18075 df-meet 18076 df-p0 18152 df-p1 18153 df-lat 18159 df-clat 18226 df-mgm 18335 df-sgrp 18384 df-mnd 18395 df-submnd 18440 df-grp 18589 df-minusg 18590 df-sbg 18591 df-subg 18761 df-cntz 18932 df-lsm 19250 df-cmn 19397 df-abl 19398 df-mgp 19730 df-ur 19747 df-ring 19794 df-oppr 19871 df-dvdsr 19892 df-unit 19893 df-invr 19923 df-dvr 19934 df-drng 20002 df-lmod 20134 df-lss 20203 df-lsp 20243 df-lvec 20374 df-oposet 37197 df-ol 37199 df-oml 37200 df-covers 37287 df-ats 37288 df-atl 37319 df-cvlat 37343 df-hlat 37372 df-llines 37519 df-lplanes 37520 df-lvols 37521 df-lines 37522 df-psubsp 37524 df-pmap 37525 df-padd 37817 df-lhyp 38009 df-laut 38010 df-ldil 38125 df-ltrn 38126 df-trl 38180 df-tendo 38776 df-edring 38778 df-disoa 39050 df-dvech 39100 df-dib 39160 df-dic 39194 df-dih 39250

This theorem is referenced by: dihopelvalc 39270

W3C validator