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 41236

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 41224	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐼‘𝑋) = ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))))
13	12	eleq2d 2814	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ (𝐼‘𝑋) ↔ ⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊)))))
14		simp1 1136	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
15		simp3l 1202	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
16		dihopelvalcp.v	. . . . 5 ⊢ 𝑉 = (LSubSp‘𝑈)
17	2, 5, 6, 10, 9, 16	diclss 41181	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐶‘𝑄) ∈ 𝑉)
18	14, 15, 17	syl2anc 584	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝐶‘𝑄) ∈ 𝑉)
19		simp1l 1198	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ HL)
20	19	hllatd 39351	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝐾 ∈ Lat)
21		simp2l 1200	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑋 ∈ 𝐵)
22		simp1r 1199	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐻)
23	1, 6	lhpbase 39986	. . . . . 6 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
24	22, 23	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → 𝑊 ∈ 𝐵)
25	1, 4	latmcl 18382	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ∈ 𝐵)
26	20, 21, 24, 25	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ∈ 𝐵)
27	1, 2, 4	latmle2 18407	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑊)
28	20, 21, 24, 27	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑋 ∧ 𝑊) ≤ 𝑊)
29	1, 2, 6, 10, 8, 16	diblss 41158	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
30	14, 26, 28, 29	syl12anc 836	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉)
31		dihopelvalcp.d	. . . 4 ⊢ + = (+_g‘𝑈)
32	6, 10, 31, 16, 11	dvhopellsm 41105	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐶‘𝑄) ∈ 𝑉 ∧ (𝑁‘(𝑋 ∧ 𝑊)) ∈ 𝑉) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
33	14, 18, 30, 32	syl3anc 1373	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝐹, 𝑆⟩ ∈ ((𝐶‘𝑄) ⊕ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
34		dihopelvalcp.p	. . . . . . . . 9 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
35		dihopelvalcp.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
36		dihopelvalcp.e	. . . . . . . . 9 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
37		dihopelvalcp.g	. . . . . . . . 9 ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)
38		vex 3448	. . . . . . . . 9 ⊢ 𝑥 ∈ V
39		vex 3448	. . . . . . . . 9 ⊢ 𝑦 ∈ V
40	2, 5, 6, 34, 35, 36, 9, 37, 38, 39	dicopelval2 41169	. . . . . . . 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 41136	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∧ 𝑊) ∈ 𝐵 ∧ (𝑋 ∧ 𝑊) ≤ 𝑊)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
45	14, 26, 28, 44	syl12anc 836	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊)) ↔ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)))
46	41, 45	anbi12d 632	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → ((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ↔ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))))
47	46	anbi1d 631	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩))))
48		simpl1 1192	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
49		simprll 778	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑦‘𝐺))
50		simprlr 779	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑦 ∈ 𝐸)
51	2, 5, 6, 34	lhpocnel2 40007	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
52	48, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
53		simpl3l 1229	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
54	2, 5, 6, 35, 37	ltrniotacl 40567	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐺 ∈ 𝑇)
55	48, 52, 53, 54	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝐺 ∈ 𝑇)
56	6, 35, 36	tendocl 40755	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑦‘𝐺) ∈ 𝑇)
57	48, 50, 55, 56	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦‘𝐺) ∈ 𝑇)
58	49, 57	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑥 ∈ 𝑇)
59		simprll 778	. . . . . . . . . . . 12 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → 𝑧 ∈ 𝑇)
60	59	adantl 481	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑧 ∈ 𝑇)
61		simprrr 781	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
62	1, 6, 35, 36, 43	tendo0cl 40778	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑍 ∈ 𝐸)
63	48, 62	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑍 ∈ 𝐸)
64	61, 63	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → 𝑤 ∈ 𝐸)
65		eqid 2729	. . . . . . . . . . . 12 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
66		eqid 2729	. . . . . . . . . . . 12 ⊢ (+_g‘(Scalar‘𝑈)) = (+_g‘(Scalar‘𝑈))
67	6, 35, 36, 10, 65, 31, 66	dvhopvadd 41081	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑧 ∈ 𝑇 ∧ 𝑤 ∈ 𝐸)) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
68	48, 58, 50, 60, 64, 67	syl122anc 1381	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩)
69		dihopelvalcp.o	. . . . . . . . . . . . . 14 ⊢ 𝑂 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (ℎ ∈ 𝑇 ↦ ((𝑎‘ℎ) ∘ (𝑏‘ℎ))))
70	6, 35, 36, 10, 65, 69, 66	dvhfplusr 41072	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (+_g‘(Scalar‘𝑈)) = 𝑂)
71	48, 70	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (+_g‘(Scalar‘𝑈)) = 𝑂)
72	71	oveqd 7386	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦(+_g‘(Scalar‘𝑈))𝑤) = (𝑦𝑂𝑤))
73	72	opeq2d 4840	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → ⟨(𝑥 ∘ 𝑧), (𝑦(+_g‘(Scalar‘𝑈))𝑤)⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
74	68, 73	eqtrd 2764	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩)
75	74	eqeq2d 2740	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩) ↔ ⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩))
76		dihopelvalcp.f	. . . . . . . . . 10 ⊢ 𝐹 ∈ V
77		dihopelvalcp.s	. . . . . . . . . 10 ⊢ 𝑆 ∈ V
78	76, 77	opth 5431	. . . . . . . . 9 ⊢ (⟨𝐹, 𝑆⟩ = ⟨(𝑥 ∘ 𝑧), (𝑦𝑂𝑤)⟩ ↔ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = (𝑦𝑂𝑤)))
79	61	oveq2d 7385	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = (𝑦𝑂𝑍))
80	1, 6, 35, 36, 43, 69	tendo0plr 40780	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝐸) → (𝑦𝑂𝑍) = 𝑦)
81	48, 50, 80	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑍) = 𝑦)
82	79, 81	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑦𝑂𝑤) = 𝑦)
83	82	eqeq2d 2740	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))) → (𝑆 = (𝑦𝑂𝑤) ↔ 𝑆 = 𝑦))
84	83	anbi2d 630	. . . . . . . . 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 774	. . . . . . . . . . 11 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑥 = (𝑦‘𝐺))
89	88	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
90		simprrr 781	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 = 𝑦)
91	90	fveq1d 6842	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) = (𝑦‘𝐺))
92	89, 91	eqtr4d 2767	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑆‘𝐺))
93	90	eqcomd 2735	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 = 𝑆)
94		coass 6226	. . . . . . . . . . 11 ⊢ ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧))
95		simpl1 1192	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
96		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)) → 𝑦 ∈ 𝐸)
97	96	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
98	90, 97	eqeltrd 2828	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑆 ∈ 𝐸)
99	55	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
100	6, 35, 36	tendocl 40755	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑆‘𝐺) ∈ 𝑇)
101	95, 98, 99, 100	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺) ∈ 𝑇)
102	1, 6, 35	ltrn1o 40112	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
103	95, 101, 102	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
104		f1ococnv1 6811	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝐺):𝐵–1-1-onto→𝐵 → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
106	105	coeq1d 5815	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧) = (( I ↾ 𝐵) ∘ 𝑧))
107	59	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
108	1, 6, 35	ltrn1o 40112	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → 𝑧:𝐵–1-1-onto→𝐵)
109	95, 107, 108	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧:𝐵–1-1-onto→𝐵)
110		f1of 6782	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵–1-1-onto→𝐵 → 𝑧:𝐵⟶𝐵)
111		fcoi2 6717	. . . . . . . . . . . . 13 ⊢ (𝑧:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
112	109, 110, 111	3syl 18	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (( I ↾ 𝐵) ∘ 𝑧) = 𝑧)
113	106, 112	eqtr2d 2765	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = ((^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) ∘ 𝑧))
114		simprrl 780	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
115	92	coeq1d 5815	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ 𝑧))
116	114, 115	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = ((𝑆‘𝐺) ∘ 𝑧))
117	116	coeq1d 5815	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
118	6, 35	ltrncnv 40134	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇) → ^◡(𝑆‘𝐺) ∈ 𝑇)
119	95, 101, 118	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ^◡(𝑆‘𝐺) ∈ 𝑇)
120	6, 35	ltrnco 40707	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
121	95, 101, 107, 120	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇)
122	6, 35	ltrncom 40726	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡(𝑆‘𝐺) ∈ 𝑇 ∧ ((𝑆‘𝐺) ∘ 𝑧) ∈ 𝑇) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
123	95, 119, 121, 122	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)) = (((𝑆‘𝐺) ∘ 𝑧) ∘ ^◡(𝑆‘𝐺)))
124	117, 123	eqtr4d 2767	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐹 ∘ ^◡(𝑆‘𝐺)) = (^◡(𝑆‘𝐺) ∘ ((𝑆‘𝐺) ∘ 𝑧)))
125	94, 113, 124	3eqtr4a 2790	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
126		simplrr 777	. . . . . . . . . . 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 780	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 = (𝑥 ∘ 𝑧))
134		simpll1 1213	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
135	88	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 = (𝑦‘𝐺))
136	96	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑦 ∈ 𝐸)
137	134, 51	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
138		simpl3l 1229	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
139	138	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
140	134, 137, 139, 54	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐺 ∈ 𝑇)
141	134, 136, 140, 56	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑦‘𝐺) ∈ 𝑇)
142	135, 141	eqeltrd 2828	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑥 ∈ 𝑇)
143	59	ad2antrl 728	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑧 ∈ 𝑇)
144	6, 35	ltrnco 40707	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑥 ∈ 𝑇 ∧ 𝑧 ∈ 𝑇) → (𝑥 ∘ 𝑧) ∈ 𝑇)
145	134, 142, 143, 144	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑥 ∘ 𝑧) ∈ 𝑇)
146	133, 145	eqeltrd 2828	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐹 ∈ 𝑇)
147		simpl1l 1225	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝐾 ∈ HL)
148	147	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ HL)
149	148	hllatd 39351	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝐾 ∈ Lat)
150	1, 6, 35, 42	trlcl 40152	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ∈ 𝐵)
151	134, 143, 150	syl2anc 584	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ∈ 𝐵)
152		simpl2l 1227	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑋 ∈ 𝐵)
153	152	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑋 ∈ 𝐵)
154		simpl1r 1226	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑊 ∈ 𝐻)
155	154	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐻)
156	155, 23	syl 17	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → 𝑊 ∈ 𝐵)
157	149, 153, 156, 25	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ∈ 𝐵)
158		simprlr 779	. . . . . . . . . . 11 ⊢ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
159	158	ad2antrl 728	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
160	1, 2, 4	latmle1 18406	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) → (𝑋 ∧ 𝑊) ≤ 𝑋)
161	149, 153, 156, 160	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑋 ∧ 𝑊) ≤ 𝑋)
162	1, 2, 149, 151, 157, 153, 159, 161	lattrd 18388	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → (𝑅‘𝑧) ≤ 𝑋)
163	146, 136, 162	jca31 514	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))) → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))
164		simprll 778	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑥 = (𝑆‘𝐺))
165	164	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑆‘𝐺))
166		simprlr 779	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑦 = 𝑆)
167	166	adantr 480	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 = 𝑆)
168	167	fveq1d 6842	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑦‘𝐺) = (𝑆‘𝐺))
169	165, 168	eqtr4d 2767	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑥 = (𝑦‘𝐺))
170		simprlr 779	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑦 ∈ 𝐸)
171	169, 170	jca 511	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸))
172		simprrl 780	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
173	172	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)))
174		simpll1 1213	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
175		simprll 778	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 ∈ 𝑇)
176	167, 170	eqeltrrd 2829	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 ∈ 𝐸)
177	174, 51	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
178	138	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
179	174, 177, 178, 54	syl3anc 1373	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐺 ∈ 𝑇)
180	174, 176, 179, 100	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺) ∈ 𝑇)
181	174, 180, 118	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ^◡(𝑆‘𝐺) ∈ 𝑇)
182	6, 35	ltrnco 40707	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ^◡(𝑆‘𝐺) ∈ 𝑇) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
183	174, 175, 181, 182	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇)
184	173, 183	eqeltrd 2828	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑧 ∈ 𝑇)
185		simprr 772	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑋)
186	2, 6, 35, 42	trlle 40172	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇) → (𝑅‘𝑧) ≤ 𝑊)
187	174, 184, 186	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ 𝑊)
188	147	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ HL)
189	188	hllatd 39351	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐾 ∈ Lat)
190	174, 184, 150	syl2anc 584	. . . . . . . . . . . 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 18408	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝑧) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
195	189, 190, 191, 193, 194	syl13anc 1374	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑅‘𝑧) ≤ 𝑋 ∧ (𝑅‘𝑧) ≤ 𝑊) ↔ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)))
196	185, 187, 195	mpbi2and 712	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊))
197		simprrr 781	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) → 𝑤 = 𝑍)
198	197	adantr 480	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑤 = 𝑍)
199	184, 196, 198	jca31 514	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍))
200	174, 180, 102	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑆‘𝐺):𝐵–1-1-onto→𝐵)
201	200, 104	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)) = ( I ↾ 𝐵))
202	201	coeq2d 5816	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))) = (𝐹 ∘ ( I ↾ 𝐵)))
203	1, 6, 35	ltrn1o 40112	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → 𝐹:𝐵–1-1-onto→𝐵)
204	174, 175, 203	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹:𝐵–1-1-onto→𝐵)
205		f1of 6782	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵–1-1-onto→𝐵 → 𝐹:𝐵⟶𝐵)
206		fcoi1 6716	. . . . . . . . . . . . . . 15 ⊢ (𝐹:𝐵⟶𝐵 → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
207	204, 205, 206	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 ∘ ( I ↾ 𝐵)) = 𝐹)
208	202, 207	eqtr2d 2765	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺))))
209		coass 6226	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)) = (𝐹 ∘ (^◡(𝑆‘𝐺) ∘ (𝑆‘𝐺)))
210	208, 209	eqtr4di 2782	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
211	6, 35	ltrncom 40726	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝐺) ∈ 𝑇 ∧ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ 𝑇) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
212	174, 180, 183, 211	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))) = ((𝐹 ∘ ^◡(𝑆‘𝐺)) ∘ (𝑆‘𝐺)))
213	210, 212	eqtr4d 2767	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
214	165, 173	coeq12d 5818	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝑥 ∘ 𝑧) = ((𝑆‘𝐺) ∘ (𝐹 ∘ ^◡(𝑆‘𝐺))))
215	213, 214	eqtr4d 2767	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝐹 = (𝑥 ∘ 𝑧))
216	167	eqcomd 2735	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → 𝑆 = 𝑦)
217	215, 216	jca 511	. . . . . . . . 9 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦))
218	171, 199, 217	jca31 514	. . . . . . . 8 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) ∧ ((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍))) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)) → (((𝑥 = (𝑦‘𝐺) ∧ 𝑦 ∈ 𝐸) ∧ ((𝑧 ∈ 𝑇 ∧ (𝑅‘𝑧) ≤ (𝑋 ∧ 𝑊)) ∧ 𝑤 = 𝑍)) ∧ (𝐹 = (𝑥 ∘ 𝑧) ∧ 𝑆 = 𝑦)))
219	163, 218	impbida 800	. . . . . . 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 1926	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) → (∃𝑥∃𝑦∃𝑧∃𝑤((⟨𝑥, 𝑦⟩ ∈ (𝐶‘𝑄) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑁‘(𝑋 ∧ 𝑊))) ∧ ⟨𝐹, 𝑆⟩ = (⟨𝑥, 𝑦⟩ + ⟨𝑧, 𝑤⟩)) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = (𝑆‘𝐺) ∧ 𝑦 = 𝑆) ∧ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) ∧ 𝑤 = 𝑍) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋))))
225		fvex 6853	. . . 4 ⊢ (𝑆‘𝐺) ∈ V
226	225	cnvex 7881	. . . . 5 ⊢ ^◡(𝑆‘𝐺) ∈ V
227	76, 226	coex 7886	. . . 4 ⊢ (𝐹 ∘ ^◡(𝑆‘𝐺)) ∈ V
228	35	fvexi 6854	. . . . . 6 ⊢ 𝑇 ∈ V
229	228	mptex 7179	. . . . 5 ⊢ (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V
230	43, 229	eqeltri 2824	. . . 4 ⊢ 𝑍 ∈ V
231		biidd 262	. . . 4 ⊢ (𝑥 = (𝑆‘𝐺) → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
232		eleq1 2816	. . . . . 6 ⊢ (𝑦 = 𝑆 → (𝑦 ∈ 𝐸 ↔ 𝑆 ∈ 𝐸))
233	232	anbi2d 630	. . . . 5 ⊢ (𝑦 = 𝑆 → ((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ↔ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)))
234	233	anbi1d 631	. . . 4 ⊢ (𝑦 = 𝑆 → (((𝐹 ∈ 𝑇 ∧ 𝑦 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋)))
235		fveq2 6840	. . . . . 6 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (𝑅‘𝑧) = (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))))
236	235	breq1d 5112	. . . . 5 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → ((𝑅‘𝑧) ≤ 𝑋 ↔ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋))
237	236	anbi2d 630	. . . 4 ⊢ (𝑧 = (𝐹 ∘ ^◡(𝑆‘𝐺)) → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘𝑧) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
238		biidd 262	. . . 4 ⊢ (𝑤 = 𝑍 → (((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸) ∧ (𝑅‘(𝐹 ∘ ^◡(𝑆‘𝐺))) ≤ 𝑋)))
239	225, 77, 227, 230, 231, 234, 237, 238	ceqsex4v 3501	. . 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 1086 = wceq 1540 ∃wex 1779 ∈ wcel 2109 Vcvv 3444 ⟨cop 4591 class class class wbr 5102 ↦ cmpt 5183 I cid 5525 ^◡ccnv 5630 ↾ cres 5633 ∘ ccom 5635 ⟶wf 6495 –1-1-onto→wf1o 6498 ‘cfv 6499 ℩crio 7325 (class class class)co 7369 ∈ cmpo 7371 Basecbs 17156 +_gcplusg 17197 Scalarcsca 17200 lecple 17204 occoc 17205 joincjn 18253 meetcmee 18254 Latclat 18373 LSSumclsm 19549 LSubSpclss 20870 Atomscatm 39250 HLchlt 39337 LHypclh 39972 LTrncltrn 40089 trLctrl 40146 TEndoctendo 40740 DVecHcdvh 41066 DIsoBcdib 41126 DIsoCcdic 41160 DIsoHcdih 41216

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11102 ax-resscn 11103 ax-1cn 11104 ax-icn 11105 ax-addcl 11106 ax-addrcl 11107 ax-mulcl 11108 ax-mulrcl 11109 ax-mulcom 11110 ax-addass 11111 ax-mulass 11112 ax-distr 11113 ax-i2m1 11114 ax-1ne0 11115 ax-1rid 11116 ax-rnegex 11117 ax-rrecex 11118 ax-cnre 11119 ax-pre-lttri 11120 ax-pre-lttrn 11121 ax-pre-ltadd 11122 ax-pre-mulgt0 11123 ax-riotaBAD 38940

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-iin 4954 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-tpos 8182 df-undef 8229 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-pnf 11188 df-mnf 11189 df-xr 11190 df-ltxr 11191 df-le 11192 df-sub 11385 df-neg 11386 df-nn 12165 df-2 12227 df-3 12228 df-4 12229 df-5 12230 df-6 12231 df-n0 12421 df-z 12508 df-uz 12772 df-fz 13447 df-struct 17094 df-sets 17111 df-slot 17129 df-ndx 17141 df-base 17157 df-ress 17178 df-plusg 17210 df-mulr 17211 df-sca 17213 df-vsca 17214 df-0g 17381 df-proset 18236 df-poset 18255 df-plt 18270 df-lub 18286 df-glb 18287 df-join 18288 df-meet 18289 df-p0 18365 df-p1 18366 df-lat 18374 df-clat 18441 df-mgm 18550 df-sgrp 18629 df-mnd 18645 df-submnd 18694 df-grp 18851 df-minusg 18852 df-sbg 18853 df-subg 19038 df-cntz 19232 df-lsm 19551 df-cmn 19697 df-abl 19698 df-mgp 20062 df-rng 20074 df-ur 20103 df-ring 20156 df-oppr 20258 df-dvdsr 20278 df-unit 20279 df-invr 20309 df-dvr 20322 df-drng 20652 df-lmod 20801 df-lss 20871 df-lsp 20911 df-lvec 21043 df-oposet 39163 df-ol 39165 df-oml 39166 df-covers 39253 df-ats 39254 df-atl 39285 df-cvlat 39309 df-hlat 39338 df-llines 39486 df-lplanes 39487 df-lvols 39488 df-lines 39489 df-psubsp 39491 df-pmap 39492 df-padd 39784 df-lhyp 39976 df-laut 39977 df-ldil 40092 df-ltrn 40093 df-trl 40147 df-tendo 40743 df-edring 40745 df-disoa 41017 df-dvech 41067 df-dib 41127 df-dic 41161 df-dih 41217

This theorem is referenced by: dihopelvalc 41237

W3C validator