cdlemk12 - Mathbox for Norm Megill

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

Theorem cdlemk12 41313

Description: Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.)

**Hypotheses**
Ref	Expression
cdlemk.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk.l	⊢ ≤ = (le‘𝐾)
cdlemk.j	⊢ ∨ = (join‘𝐾)
cdlemk.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk.m	⊢ ∧ = (meet‘𝐾)
cdlemk.s	⊢ 𝑆 = (𝑓 ∈ 𝑇 ↦ (℩𝑖 ∈ 𝑇 (𝑖‘𝑃) = ((𝑃 ∨ (𝑅‘𝑓)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑓 ∘ ^◡𝐹))))))

**Assertion**
Ref	Expression
cdlemk12	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺)))))

Distinct variable groups: ∧ ,𝑓 ∨ ,𝑓 𝑓,𝐹,𝑖 𝑓,𝐺,𝑖 𝑓,𝑁 𝑃,𝑓 𝑅,𝑓 𝑇,𝑓 𝑓,𝑊 ∧ ,𝑖 ≤ ,𝑖 ∨ ,𝑖 𝐴,𝑖 𝑖,𝐹 𝑖,𝐻 𝑖,𝐾 𝑖,𝑁 𝑃,𝑖 𝑅,𝑖 𝑇,𝑖 𝑖,𝑊 𝑓,𝑋,𝑖 Allowed substitution hints: 𝐴(𝑓) 𝐵(𝑓,𝑖) 𝑆(𝑓,𝑖) 𝐻(𝑓) 𝐾(𝑓) ≤ (𝑓)

**Proof of Theorem cdlemk12**
Step	Hyp	Ref	Expression
1		simp11l 1286	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐾 ∈ HL)
2		simp22l 1294	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑃 ∈ 𝐴)
3		simp11 1205	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4		simp13 1207	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐺 ∈ 𝑇)
5		cdlemk.l	. . . 4 ⊢ ≤ = (le‘𝐾)
6		cdlemk.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
7		cdlemk.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
8		cdlemk.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9	5, 6, 7, 8	ltrnat 40603	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴)
10	3, 4, 2, 9	syl3anc 1374	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝐺‘𝑃) ∈ 𝐴)
11		simp12 1206	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐹 ∈ 𝑇)
12		simp21r 1293	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑋 ∈ 𝑇)
13	3, 11, 12	3jca 1129	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇))
14		simp21l 1292	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑁 ∈ 𝑇)
15		simp22 1209	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
16		simp23 1210	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐹) = (𝑅‘𝑁))
17	14, 15, 16	3jca 1129	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)))
18		simp311 1322	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐹 ≠ ( I ↾ 𝐵))
19		simp313 1324	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝑋 ≠ ( I ↾ 𝐵))
20		simp32r 1301	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝑋) ≠ (𝑅‘𝐹))
21		cdlemk.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
22		cdlemk.j	. . . 4 ⊢ ∨ = (join‘𝐾)
23		cdlemk.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
24		cdlemk.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
25		cdlemk.s	. . . 4 ⊢ 𝑆 = (𝑓 ∈ 𝑇 ↦ (℩𝑖 ∈ 𝑇 (𝑖‘𝑃) = ((𝑃 ∨ (𝑅‘𝑓)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑓 ∘ ^◡𝐹))))))
26	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksat 41309	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹))) → ((𝑆‘𝑋)‘𝑃) ∈ 𝐴)
27	13, 17, 18, 19, 20, 26	syl113anc 1385	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝑋)‘𝑃) ∈ 𝐴)
28		simp33 1213	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≠ (𝑅‘𝑋))
29	28	necomd 2988	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝑋) ≠ (𝑅‘𝐺))
30	6, 7, 8, 23	trlcocnvat 41187	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐺)) → (𝑅‘(𝑋 ∘ ^◡𝐺)) ∈ 𝐴)
31	3, 12, 4, 29, 30	syl121anc 1378	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝑋 ∘ ^◡𝐺)) ∈ 𝐴)
32		simp1 1137	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇))
33		simp312 1323	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐺 ≠ ( I ↾ 𝐵))
34		simp32l 1300	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≠ (𝑅‘𝐹))
35	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksat 41309	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹))) → ((𝑆‘𝐺)‘𝑃) ∈ 𝐴)
36	32, 17, 18, 33, 34, 35	syl113anc 1385	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ∈ 𝐴)
37	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksv2 41310	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
38	32, 17, 18, 33, 34, 37	syl113anc 1385	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
39	1	hllatd 39827	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → 𝐾 ∈ Lat)
40	21, 6, 7, 8, 23	trlnidat 40636	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ 𝐴)
41	3, 4, 33, 40	syl3anc 1374	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ∈ 𝐴)
42	21, 22, 6	hlatjcl 39830	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
43	1, 2, 41, 42	syl3anc 1374	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
44	5, 6, 7, 8	ltrnat 40603	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝑁‘𝑃) ∈ 𝐴)
45	3, 14, 2, 44	syl3anc 1374	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑁‘𝑃) ∈ 𝐴)
46	6, 7, 8, 23	trlcocnvat 41187	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
47	3, 4, 11, 34, 46	syl121anc 1378	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
48	21, 22, 6	hlatjcl 39830	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑁‘𝑃) ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴) → ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
49	1, 45, 47, 48	syl3anc 1374	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
50	21, 5, 24	latmle1 18424	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵 ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ≤ (𝑃 ∨ (𝑅‘𝐺)))
51	39, 43, 49, 50	syl3anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ≤ (𝑃 ∨ (𝑅‘𝐺)))
52	38, 51	eqbrtrd 5108	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)))
53	5, 22, 6, 7, 8, 23	trljat1 40629	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝐺)) = (𝑃 ∨ (𝐺‘𝑃)))
54	3, 4, 15, 53	syl3anc 1374	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∨ (𝑅‘𝐺)) = (𝑃 ∨ (𝐺‘𝑃)))
55	52, 54	breqtrd 5112	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝐺‘𝑃)))
56		simp2 1138	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)))
57		simp31 1211	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)))
58		eqid 2737	. . . 4 ⊢ (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹)))) = (((𝐺‘𝑃) ∨ (𝑋‘𝑃)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∨ (𝑅‘(𝑋 ∘ ^◡𝐹))))
59	21, 5, 22, 6, 7, 8, 23, 24, 25, 58	cdlemk11 41312	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹))) → ((𝑆‘𝐺)‘𝑃) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))))
60	32, 56, 57, 34, 20, 59	syl113anc 1385	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))))
61	5, 22, 6	hlatlej2 39839	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)))
62	1, 2, 41, 61	syl3anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)))
63	62, 54	breqtrd 5112	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝐺‘𝑃)))
64	21, 5, 22, 6, 7, 8, 23, 24, 25	cdlemksel 41308	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹))) → (𝑆‘𝑋) ∈ 𝑇)
65	13, 17, 18, 19, 20, 64	syl113anc 1385	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑆‘𝑋) ∈ 𝑇)
66	5, 6, 7, 8	ltrnel 40602	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝑋) ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑆‘𝑋)‘𝑃) ≤ 𝑊))
67	3, 65, 15, 66	syl3anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑆‘𝑋)‘𝑃) ≤ 𝑊))
68	7, 8	ltrncnv 40609	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → ^◡𝐺 ∈ 𝑇)
69	3, 4, 68	syl2anc 585	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ^◡𝐺 ∈ 𝑇)
70	7, 8, 23	trlcnv 40628	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘^◡𝐺) = (𝑅‘𝐺))
71	3, 4, 70	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘^◡𝐺) = (𝑅‘𝐺))
72	71, 28	eqnetrd 3000	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘^◡𝐺) ≠ (𝑅‘𝑋))
73	21, 7, 8, 23	trlcone 41191	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (^◡𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ ((𝑅‘^◡𝐺) ≠ (𝑅‘𝑋) ∧ 𝑋 ≠ ( I ↾ 𝐵))) → (𝑅‘^◡𝐺) ≠ (𝑅‘(^◡𝐺 ∘ 𝑋)))
74	3, 69, 12, 72, 19, 73	syl122anc 1382	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘^◡𝐺) ≠ (𝑅‘(^◡𝐺 ∘ 𝑋)))
75	74	necomd 2988	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(^◡𝐺 ∘ 𝑋)) ≠ (𝑅‘^◡𝐺))
76	7, 8	ltrncom 41201	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) → (^◡𝐺 ∘ 𝑋) = (𝑋 ∘ ^◡𝐺))
77	3, 69, 12, 76	syl3anc 1374	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (^◡𝐺 ∘ 𝑋) = (𝑋 ∘ ^◡𝐺))
78	77	fveq2d 6839	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(^◡𝐺 ∘ 𝑋)) = (𝑅‘(𝑋 ∘ ^◡𝐺)))
79	75, 78, 71	3netr3d 3009	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝑋 ∘ ^◡𝐺)) ≠ (𝑅‘𝐺))
80	7, 8	ltrnco 41182	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑇 ∧ ^◡𝐺 ∈ 𝑇) → (𝑋 ∘ ^◡𝐺) ∈ 𝑇)
81	3, 12, 69, 80	syl3anc 1374	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑋 ∘ ^◡𝐺) ∈ 𝑇)
82	5, 7, 8, 23	trlle 40647	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∘ ^◡𝐺) ∈ 𝑇) → (𝑅‘(𝑋 ∘ ^◡𝐺)) ≤ 𝑊)
83	3, 81, 82	syl2anc 585	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘(𝑋 ∘ ^◡𝐺)) ≤ 𝑊)
84	5, 7, 8, 23	trlle 40647	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ≤ 𝑊)
85	3, 4, 84	syl2anc 585	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑅‘𝐺) ≤ 𝑊)
86	5, 22, 6, 7	lhp2atnle 40496	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑆‘𝑋)‘𝑃) ≤ 𝑊) ∧ (𝑅‘(𝑋 ∘ ^◡𝐺)) ≠ (𝑅‘𝐺)) ∧ ((𝑅‘(𝑋 ∘ ^◡𝐺)) ∈ 𝐴 ∧ (𝑅‘(𝑋 ∘ ^◡𝐺)) ≤ 𝑊) ∧ ((𝑅‘𝐺) ∈ 𝐴 ∧ (𝑅‘𝐺) ≤ 𝑊)) → ¬ (𝑅‘𝐺) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))))
87	3, 67, 79, 31, 83, 41, 85, 86	syl322anc 1401	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ¬ (𝑅‘𝐺) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))))
88		nbrne1 5105	. . 3 ⊢ (((𝑅‘𝐺) ≤ (𝑃 ∨ (𝐺‘𝑃)) ∧ ¬ (𝑅‘𝐺) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺)))) → (𝑃 ∨ (𝐺‘𝑃)) ≠ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))))
89	63, 87, 88	syl2anc 585	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → (𝑃 ∨ (𝐺‘𝑃)) ≠ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))))
90	5, 22, 24, 6	2atm 39990	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐺‘𝑃) ∈ 𝐴) ∧ (((𝑆‘𝑋)‘𝑃) ∈ 𝐴 ∧ (𝑅‘(𝑋 ∘ ^◡𝐺)) ∈ 𝐴 ∧ ((𝑆‘𝐺)‘𝑃) ∈ 𝐴) ∧ (((𝑆‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝐺‘𝑃)) ∧ ((𝑆‘𝐺)‘𝑃) ≤ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))) ∧ (𝑃 ∨ (𝐺‘𝑃)) ≠ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺))))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺)))))
91	1, 2, 10, 27, 31, 36, 55, 60, 89, 90	syl333anc 1405	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑁 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑋 ≠ ( I ↾ 𝐵)) ∧ ((𝑅‘𝐺) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑋) ≠ (𝑅‘𝐹)) ∧ (𝑅‘𝐺) ≠ (𝑅‘𝑋))) → ((𝑆‘𝐺)‘𝑃) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ (((𝑆‘𝑋)‘𝑃) ∨ (𝑅‘(𝑋 ∘ ^◡𝐺)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 class class class wbr 5086 ↦ cmpt 5167 I cid 5519 ^◡ccnv 5624 ↾ cres 5627 ∘ ccom 5629 ‘cfv 6493 ℩crio 7317 (class class class)co 7361 Basecbs 17173 lecple 17221 joincjn 18271 meetcmee 18272 Latclat 18391 Atomscatm 39726 HLchlt 39813 LHypclh 40447 LTrncltrn 40564 trLctrl 40621

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 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-riotaBAD 39416

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-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5520 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-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 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-1st 7936 df-2nd 7937 df-undef 8217 df-map 8769 df-proset 18254 df-poset 18273 df-plt 18288 df-lub 18304 df-glb 18305 df-join 18306 df-meet 18307 df-p0 18383 df-p1 18384 df-lat 18392 df-clat 18459 df-oposet 39639 df-ol 39641 df-oml 39642 df-covers 39729 df-ats 39730 df-atl 39761 df-cvlat 39785 df-hlat 39814 df-llines 39961 df-lplanes 39962 df-lvols 39963 df-lines 39964 df-psubsp 39966 df-pmap 39967 df-padd 40259 df-lhyp 40451 df-laut 40452 df-ldil 40567 df-ltrn 40568 df-trl 40622

This theorem is referenced by: cdlemk21N 41336 cdlemk20 41337

W3C validator