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 41576

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 41564	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))))
13	12	eleq2d 2823	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊)))))
14		simp1 1137	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
15		simp3l 1203	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
16		dihopelvalcp.v	. . . . 5 ⊢ 𝑉 = (LSubSp‘𝑈)
17	2, 5, 6, 10, 9, 16	diclss 41521	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐶‘𝑄) ∈ 𝑉)
18	14, 15, 17	syl2anc 585	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐶‘𝑄) ∈ 𝑉)
19		simp1l 1199	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
20	19	hllatd 39692	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
21		simp2l 1201	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
22		simp1r 1200	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
23	1, 6	lhpbase 40326	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
24	22, 23	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
25	1, 4	latmcl 18367	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
26	20, 21, 24, 25	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
27	1, 2, 4	latmle2 18392	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊)
28	20, 21, 24, 27	syl3anc 1374	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ≤ 𝑊)
29	1, 2, 6, 10, 8, 16	diblss 41498	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
30	14, 26, 28, 29	syl12anc 837	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
31		dihopelvalcp.d	. . . 4 ⊢ + = (+_g‘𝑈)
32	6, 10, 31, 16, 11	dvhopellsm 41445	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶‘𝑄) ∈ 𝑉 ∧ (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
33	14, 18, 30, 32	syl3anc 1374	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
34		dihopelvalcp.p	. . . . . . . . 9 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
35		dihopelvalcp.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
36		dihopelvalcp.e	. . . . . . . . 9 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
37		dihopelvalcp.g	. . . . . . . . 9 ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
38		vex 3445	. . . . . . . . 9 ⊢ 𝑥 ∈ V
39		vex 3445	. . . . . . . . 9 ⊢ 𝑦 ∈ V
40	2, 5, 6, 34, 35, 36, 9, 37, 38, 39	dicopelval2 41509	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
41	14, 15, 40	syl2anc 585	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ↔ (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸)))
42		dihopelvalcp.r	. . . . . . . . 9 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
43		dihopelvalcp.z	. . . . . . . . 9 ⊢ 𝑍 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
44	1, 2, 6, 35, 42, 43, 8	dibopelval3 41476	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
45	14, 26, 28, 44	syl12anc 837	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
46	41, 45	anbi12d 633	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))))
47	46	anbi1d 632	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
48		simpl1 1193	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
49		simprll 779	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑦‘𝐺))
50		simprlr 780	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑦 ∈ 𝐸)
51	2, 5, 6, 34	lhpocnel2 40347	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
52	48, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53		simpl3l 1230	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
54	2, 5, 6, 35, 37	ltrniotacl 40907	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
55	48, 52, 53, 54	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝐺 ∈ 𝑇)
56	6, 35, 36	tendocl 41095	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑦‘𝐺) ∈ 𝑇)
57	48, 50, 55, 56	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦‘𝐺) ∈ 𝑇)
58	49, 57	eqeltrd 2837	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 ∈ 𝑇)
59		simprll 779	. . . . . . . . . . . 12 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → 𝑧 ∈ 𝑇)
60	59	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑧 ∈ 𝑇)
61		simprrr 782	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
62	1, 6, 35, 36, 43	tendo0cl 41118	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑍 ∈ 𝐸)
63	48, 62	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑍 ∈ 𝐸)
64	61, 63	eqeltrd 2837	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 ∈ 𝐸)
65		eqid 2737	. . . . . . . . . . . 12 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
66		eqid 2737	. . . . . . . . . . . 12 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
67	6, 35, 36, 10, 65, 31, 66	dvhopvadd 41421	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑧 ∈ 𝑇 ∧ 𝑤 ∈ 𝐸)) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
68	48, 58, 50, 60, 64, 67	syl122anc 1382	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
69		dihopelvalcp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑎‘ℎ) ∘ (𝑏‘ℎ))))
70	6, 35, 36, 10, 65, 69, 66	dvhfplusr 41412	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+_g‘(Scalar‘𝑈)) = 𝑂)
71	48, 70	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (+_g‘(Scalar‘𝑈)) = 𝑂)
72	71	oveqd 7377	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦(+_g‘(Scalar‘𝑈))𝑤) = (𝑦𝑂𝑤))
73	72	opeq2d 4837	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
74	68, 73	eqtrd 2772	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
75	74	eqeq2d 2748	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩))
76		dihopelvalcp.f	. . . . . . . . . 10 ⊢ 𝐹 ∈ V
77		dihopelvalcp.s	. . . . . . . . . 10 ⊢ 𝑆 ∈ V
78	76, 77	opth 5425	. . . . . . . . 9 ⊢ (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)))
79	61	oveq2d 7376	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = (𝑦𝑂𝑍))
80	1, 6, 35, 36, 43, 69	tendo0plr 41120	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸) → (𝑦𝑂𝑍) = 𝑦)
81	48, 50, 80	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑍) = 𝑦)
82	79, 81	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = 𝑦)
83	82	eqeq2d 2748	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑆 = (𝑦𝑂𝑤) ↔ 𝑆 = 𝑦))
84	83	anbi2d 631	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ((𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
85	78, 84	bitrid 283	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
86	75, 85	bitrd 279	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
87	86	pm5.32da 579	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))))
88		simplll 775	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑥 = (𝑦‘𝐺))
89	88	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
90		simprrr 782	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 = 𝑦)
91	90	fveq1d 6837	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) = (𝑦‘𝐺))
92	89, 91	eqtr4d 2775	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑆‘𝐺))
93	90	eqcomd 2743	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 = 𝑆)
94		coass 6225	. . . . . . . . . . 11 ⊢ ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧))
95		simpl1 1193	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
96		simpllr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑦 ∈ 𝐸)
97	96	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
98	90, 97	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 ∈ 𝐸)
99	55	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
100	6, 35, 36	tendocl 41095	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑆‘𝐺) ∈ 𝑇)
101	95, 98, 99, 100	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) ∈ 𝑇)
102	1, 6, 35	ltrn1o 40452	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
103	95, 101, 102	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
104		f1ococnv1 6804	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐺):𝐵–1-1-onto→𝐵 → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
106	105	coeq1d 5811	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (( I ↾ 𝐵) ∘ 𝑧))
107	59	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
108	1, 6, 35	ltrn1o 40452	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → 𝑧:𝐵–1-1-onto→𝐵)
109	95, 107, 108	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧:𝐵–1-1-onto→𝐵)
110		f1of 6775	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵–1-1-onto→𝐵 → 𝑧:𝐵⟶𝐵)
111		fcoi2 6710	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
112	109, 110, 111	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
113	106, 112	eqtr2d 2773	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧))
114		simprrl 781	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
115	92	coeq1d 5811	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ 𝑧))
116	114, 115	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = ((𝑆‘𝐺) ∘ 𝑧))
117	116	coeq1d 5811	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
118	6, 35	ltrncnv 40474	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → ^◡(𝑆‘𝐺) ∈ 𝑇)
119	95, 101, 118	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ^◡(𝑆‘𝐺) ∈ 𝑇)
120	6, 35	ltrnco 41047	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
121	95, 101, 107, 120	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
122	6, 35	ltrncom 41066	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡(𝑆‘𝐺) ∈ 𝑇 ∧ ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
123	95, 119, 121, 122	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
124	117, 123	eqtr4d 2775	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)))
125	94, 113, 124	3eqtr4a 2798	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
126		simplrr 778	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑤 = 𝑍)
127	126	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑤 = 𝑍)
128	125, 127	jca 511	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))
129	92, 93, 128	jca31 514	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)))
130	129	ex 412	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))))
131	130	pm4.71rd 562	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
132	87, 131	bitrd 279	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))))
133		simprrl 781	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
134		simpll1 1214	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
135	88	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
136	96	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
137	134, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
138		simpl3l 1230	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
139	138	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
140	134, 137, 139, 54	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
141	134, 136, 140, 56	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑦‘𝐺) ∈ 𝑇)
142	135, 141	eqeltrd 2837	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 ∈ 𝑇)
143	59	ad2antrl 729	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
144	6, 35	ltrnco 41047	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (𝑥 ∘ 𝑧) ∈ 𝑇)
145	134, 142, 143, 144	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) ∈ 𝑇)
146	133, 145	eqeltrd 2837	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 ∈ 𝑇)
147		simpl1l 1226	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝐾 ∈ HL)
148	147	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ HL)
149	148	hllatd 39692	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ Lat)
150	1, 6, 35, 42	trlcl 40492	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ∈ 𝐵)
151	134, 143, 150	syl2anc 585	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ∈ 𝐵)
152		simpl2l 1228	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑋 ∈ 𝐵)
153	152	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑋 ∈ 𝐵)
154		simpl1r 1227	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑊 ∈ 𝐻)
155	154	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐻)
156	155, 23	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐵)
157	149, 153, 156, 25	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ∈ 𝐵)
158		simprlr 780	. . . . . . . . . . 11 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
159	158	ad2antrl 729	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
160	1, 2, 4	latmle1 18391	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑋)
161	149, 153, 156, 160	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ≤ 𝑋)
162	1, 2, 149, 151, 157, 153, 159, 161	lattrd 18373	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ 𝑋)
163	146, 136, 162	jca31 514	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))
164		simprll 779	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑆‘𝐺))
165	164	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑆‘𝐺))
166		simprlr 780	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑦 = 𝑆)
167	166	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 = 𝑆)
168	167	fveq1d 6837	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑦‘𝐺) = (𝑆‘𝐺))
169	165, 168	eqtr4d 2775	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑦‘𝐺))
170		simprlr 780	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 ∈ 𝐸)
171	169, 170	jca 511	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸))
172		simprrl 781	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
173	172	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
174		simpll1 1214	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
175		simprll 779	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 ∈ 𝑇)
176	167, 170	eqeltrrd 2838	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 ∈ 𝐸)
177	174, 51	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
178	138	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
179	174, 177, 178, 54	syl3anc 1374	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐺 ∈ 𝑇)
180	174, 176, 179, 100	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺) ∈ 𝑇)
181	174, 180, 118	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ^◡(𝑆‘𝐺) ∈ 𝑇)
182	6, 35	ltrnco 41047	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ^◡(𝑆‘𝐺) ∈ 𝑇) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
183	174, 175, 181, 182	syl3anc 1374	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
184	173, 183	eqeltrd 2837	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 ∈ 𝑇)
185		simprr 773	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑋)
186	2, 6, 35, 42	trlle 40512	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ≤ 𝑊)
187	174, 184, 186	syl2anc 585	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑊)
188	147	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ HL)
189	188	hllatd 39692	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ Lat)
190	174, 184, 150	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ∈ 𝐵)
191	152	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑋 ∈ 𝐵)
192	154	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐻)
193	192, 23	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑊 ∈ 𝐵)
194	1, 2, 4	latlem12 18393	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝑧) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
195	189, 190, 191, 193, 194	syl13anc 1375	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
196	185, 187, 195	mpbi2and 713	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
197		simprrr 782	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
198	197	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑤 = 𝑍)
199	184, 196, 198	jca31 514	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))
200	174, 180, 102	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
201	200, 104	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
202	201	coeq2d 5812	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))) = (𝐹 ∘ ( I ↾ 𝐵)))
203	1, 6, 35	ltrn1o 40452	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
204	174, 175, 203	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹:𝐵–1-1-onto→𝐵)
205		f1of 6775	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹:𝐵⟶𝐵)
206		fcoi1 6709	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
207	204, 205, 206	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
208	202, 207	eqtr2d 2773	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))))
209		coass 6225	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)) = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)))
210	208, 209	eqtr4di 2790	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
211	6, 35	ltrncom 41066	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
212	174, 180, 183, 211	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
213	210, 212	eqtr4d 2775	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
214	165, 173	coeq12d 5814	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
215	213, 214	eqtr4d 2775	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝑥 ∘ 𝑧))
216	167	eqcomd 2743	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 = 𝑦)
217	215, 216	jca 511	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))
218	171, 199, 217	jca31 514	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
219	163, 218	impbida 801	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
220	219	pm5.32da 579	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
221		df-3an 1089	. . . . . 6 ⊢ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) ↔ (((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
222	220, 221	bitr4di 289	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
223	47, 132, 222	3bitrd 305	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
224	223	4exbidv 1928	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
225		fvex 6848	. . . 4 ⊢ (𝑆‘𝐺) ∈ V
226	225	cnvex 7869	. . . . 5 ⊢ ^◡(𝑆‘𝐺) ∈ V
227	76, 226	coex 7874	. . . 4 ⊢ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ V
228	35	fvexi 6849	. . . . . 6 ⊢ 𝑇 ∈ V
229	228	mptex 7171	. . . . 5 ⊢ (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V
230	43, 229	eqeltri 2833	. . . 4 ⊢ 𝑍 ∈ V
231		biidd 262	. . . 4 ⊢ (𝑥 = (𝑆‘𝐺) → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
232		eleq1 2825	. . . . . 6 ⊢ (𝑦 = 𝑆 → (𝑦 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸))
233	232	anbi2d 631	. . . . 5 ⊢ (𝑦 = 𝑆 → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ↔ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)))
234	233	anbi1d 632	. . . 4 ⊢ (𝑦 = 𝑆 → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
235		fveq2 6835	. . . . . 6 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (𝑅‘𝑧) = (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))))
236	235	breq1d 5109	. . . . 5 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → ((𝑅‘𝑧) ≤ 𝑋 ↔ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
237	236	anbi2d 631	. . . 4 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
238		biidd 262	. . . 4 ⊢ (𝑤 = 𝑍 → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
239	225, 77, 227, 230, 231, 234, 237, 238	ceqsex4v 3497	. . 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 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 Vcvv 3441 ⟨cop 4587 class class class wbr 5099 ↦ cmpt 5180 I cid 5519 ^◡ccnv 5624 ↾ cres 5627 ∘ ccom 5629 ⟶wf 6489 –1-1-onto→wf1o 6492 ‘cfv 6493 ℩crio 7316 (class class class)co 7360 ∈ cmpo 7362 Basecbs 17140 +_gcplusg 17181 Scalarcsca 17184 lecple 17188 occoc 17189 joincjn 18238 meetcmee 18239 Latclat 18358 LSSumclsm 19567 LSubSpclss 20886 Atomscatm 39591 HLchlt 39678 LHypclh 40312 LTrncltrn 40429 trLctrl 40486 TEndoctendo 41080 DVecHcdvh 41406 DIsoBcdib 41466 DIsoCcdic 41500 DIsoHcdih 41556

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7682 ax-cnex 11086 ax-resscn 11087 ax-1cn 11088 ax-icn 11089 ax-addcl 11090 ax-addrcl 11091 ax-mulcl 11092 ax-mulrcl 11093 ax-mulcom 11094 ax-addass 11095 ax-mulass 11096 ax-distr 11097 ax-i2m1 11098 ax-1ne0 11099 ax-1rid 11100 ax-rnegex 11101 ax-rrecex 11102 ax-cnre 11103 ax-pre-lttri 11104 ax-pre-lttrn 11105 ax-pre-ltadd 11106 ax-pre-mulgt0 11107 ax-riotaBAD 39281

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4904 df-iun 4949 df-iin 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-tpos 8170 df-undef 8217 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12150 df-2 12212 df-3 12213 df-4 12214 df-5 12215 df-6 12216 df-n0 12406 df-z 12493 df-uz 12756 df-fz 13428 df-struct 17078 df-sets 17095 df-slot 17113 df-ndx 17125 df-base 17141 df-ress 17162 df-plusg 17194 df-mulr 17195 df-sca 17197 df-vsca 17198 df-0g 17365 df-proset 18221 df-poset 18240 df-plt 18255 df-lub 18271 df-glb 18272 df-join 18273 df-meet 18274 df-p0 18350 df-p1 18351 df-lat 18359 df-clat 18426 df-mgm 18569 df-sgrp 18648 df-mnd 18664 df-submnd 18713 df-grp 18870 df-minusg 18871 df-sbg 18872 df-subg 19057 df-cntz 19250 df-lsm 19569 df-cmn 19715 df-abl 19716 df-mgp 20080 df-rng 20092 df-ur 20121 df-ring 20174 df-oppr 20277 df-dvdsr 20297 df-unit 20298 df-invr 20328 df-dvr 20341 df-drng 20668 df-lmod 20817 df-lss 20887 df-lsp 20927 df-lvec 21059 df-oposet 39504 df-ol 39506 df-oml 39507 df-covers 39594 df-ats 39595 df-atl 39626 df-cvlat 39650 df-hlat 39679 df-llines 39826 df-lplanes 39827 df-lvols 39828 df-lines 39829 df-psubsp 39831 df-pmap 39832 df-padd 40124 df-lhyp 40316 df-laut 40317 df-ldil 40432 df-ltrn 40433 df-trl 40487 df-tendo 41083 df-edring 41085 df-disoa 41357 df-dvech 41407 df-dib 41467 df-dic 41501 df-dih 41557

This theorem is referenced by: dihopelvalc 41577

W3C validator