cdlemh - Mathbox for Norm Megill

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

Theorem cdlemh 40855

Description: Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)

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

**Assertion**
Ref	Expression
cdlemh	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))

**Proof of Theorem cdlemh**
Step	Hyp	Ref	Expression
1		simp1 1136	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇))
2		simp21l 1291	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐴)
3		simp22l 1293	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ∈ 𝐴)
4		simp23 1209	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹)))
5		simp33 1212	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ≠ (𝑅‘𝐺))
6		cdlemh.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
7		cdlemh.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
8		cdlemh.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
9		cdlemh.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
10		cdlemh.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
11		cdlemh.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
12		cdlemh.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
13		cdlemh.r	. . . . . 6 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
14		cdlemh.s	. . . . . 6 ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
15	6, 7, 8, 9, 10, 11, 12, 13, 14	cdlemh1 40853	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
16	1, 2, 3, 4, 5, 15	syl122anc 1381	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
17		oveq1 7353	. . . . . . . 8 ⊢ (𝑆 = (0.‘𝐾) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((0.‘𝐾) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
18		simp11l 1285	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ HL)
19		hlol 39399	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ OL)
21		simp11r 1286	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑊 ∈ 𝐻)
22	18, 21	jca 511	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
23		simp13 1206	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇)
24		simp12 1205	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇)
25	11, 12	ltrncnv 40184	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
26	22, 24, 25	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ∈ 𝑇)
27	23, 26	jca 511	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇))
28	5	necomd 2983	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≠ (𝑅‘𝐹))
29	11, 12, 13	trlcnv 40203	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
30	22, 24, 29	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
31	28, 30	neeqtrrd 3002	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≠ (𝑅‘^◡𝐹))
32	10, 11, 12, 13	trlcoat 40761	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ (𝑅‘𝐺) ≠ (𝑅‘^◡𝐹)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
33	22, 27, 31, 32	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
34	6, 10	atbase 39327	. . . . . . . . . 10 ⊢ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
35	33, 34	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
36		eqid 2731	. . . . . . . . . 10 ⊢ (0.‘𝐾) = (0.‘𝐾)
37	6, 8, 36	olj02 39264	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵) → ((0.‘𝐾) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
38	20, 35, 37	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((0.‘𝐾) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
39	17, 38	sylan9eqr 2788	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ 𝑆 = (0.‘𝐾)) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
40	11, 12	ltrnco 40757	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
41	22, 23, 26, 40	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
42	7, 11, 12, 13	trlle 40222	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
43	22, 41, 42	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
44		simp22r 1294	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ 𝑄 ≤ 𝑊)
45		nbrne2 5111	. . . . . . . . . . . . 13 ⊢ (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ 𝑄)
46	45	necomd 2983	. . . . . . . . . . . 12 ⊢ (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊) → 𝑄 ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
47	43, 44, 46	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
48		eqid 2731	. . . . . . . . . . . 12 ⊢ (LLines‘𝐾) = (LLines‘𝐾)
49	8, 10, 48	llni2 39550	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴) ∧ 𝑄 ≠ (𝑅‘(𝐺 ∘ ^◡𝐹))) → (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ (LLines‘𝐾))
50	18, 3, 33, 47, 49	syl31anc 1375	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ (LLines‘𝐾))
51	10, 48	llnneat 39552	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ (LLines‘𝐾)) → ¬ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐴)
52	18, 50, 51	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐴)
53		nelne2 3026	. . . . . . . . 9 ⊢ (((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 ∧ ¬ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐴) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
54	33, 52, 53	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
55	54	adantr 480	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ 𝑆 = (0.‘𝐾)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
56	39, 55	eqnetrd 2995	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ 𝑆 = (0.‘𝐾)) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
57	56	ex 412	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 = (0.‘𝐾) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
58	57	necon2d 2951	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) → 𝑆 ≠ (0.‘𝐾)))
59	16, 58	mpd 15	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑆 ≠ (0.‘𝐾))
60		simp32 1211	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ≠ ( I ↾ 𝐵))
61	6, 10, 11, 12, 13	trlnidat 40211	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ 𝐴)
62	22, 23, 60, 61	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ 𝐴)
63	7, 8, 10	hlatlej2 39414	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)))
64	18, 2, 62, 63	syl3anc 1373	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)))
65		simp22 1208	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
66		simp31 1210	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ≠ ( I ↾ 𝐵))
67	6, 11, 12	ltrncnvnid 40165	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → ^◡𝐹 ≠ ( I ↾ 𝐵))
68	22, 24, 66, 67	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ≠ ( I ↾ 𝐵))
69	6, 11, 12, 13	trlcone 40766	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ ((𝑅‘𝐺) ≠ (𝑅‘^◡𝐹) ∧ ^◡𝐹 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐺) ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
70	69	necomd 2983	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ ((𝑅‘𝐺) ≠ (𝑅‘^◡𝐹) ∧ ^◡𝐹 ≠ ( I ↾ 𝐵))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑅‘𝐺))
71	22, 23, 26, 31, 68, 70	syl122anc 1381	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑅‘𝐺))
72	7, 11, 12, 13	trlle 40222	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ≤ 𝑊)
73	22, 23, 72	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≤ 𝑊)
74	7, 8, 10, 11	lhp2atnle 40071	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑅‘𝐺)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊) ∧ ((𝑅‘𝐺) ∈ 𝐴 ∧ (𝑅‘𝐺) ≤ 𝑊)) → ¬ (𝑅‘𝐺) ≤ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
75	22, 65, 71, 33, 43, 62, 73, 74	syl322anc 1400	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ (𝑅‘𝐺) ≤ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
76		nbrne1 5110	. . . . . . . 8 ⊢ (((𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)) ∧ ¬ (𝑅‘𝐺) ≤ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) → (𝑃 ∨ (𝑅‘𝐺)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
77	64, 75, 76	syl2anc 584	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∨ (𝑅‘𝐺)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
78	8, 9, 36, 10	2atmat0 39564	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 ∧ (𝑃 ∨ (𝑅‘𝐺)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾)))
79	18, 2, 62, 3, 33, 77, 78	syl33anc 1387	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾)))
80	14	eleq1i 2822	. . . . . . 7 ⊢ (𝑆 ∈ 𝐴 ↔ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴)
81	14	eqeq1i 2736	. . . . . . 7 ⊢ (𝑆 = (0.‘𝐾) ↔ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾))
82	80, 81	orbi12i 914	. . . . . 6 ⊢ ((𝑆 ∈ 𝐴 ∨ 𝑆 = (0.‘𝐾)) ↔ (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾)))
83	79, 82	sylibr 234	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∈ 𝐴 ∨ 𝑆 = (0.‘𝐾)))
84	83	ord 864	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (¬ 𝑆 ∈ 𝐴 → 𝑆 = (0.‘𝐾)))
85	84	necon1ad 2945	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ≠ (0.‘𝐾) → 𝑆 ∈ 𝐴))
86	59, 85	mpd 15	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑆 ∈ 𝐴)
87		simp21 1207	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
88	87, 65	jca 511	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)))
89	6, 7, 8, 9, 10, 11, 12, 13, 14, 36	cdlemh2 40854	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∧ 𝑊) = (0.‘𝐾))
90	88, 89	syld3an2 1413	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∧ 𝑊) = (0.‘𝐾))
91	7, 9, 36, 10, 11	lhpmatb 40069	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐴) → (¬ 𝑆 ≤ 𝑊 ↔ (𝑆 ∧ 𝑊) = (0.‘𝐾)))
92	18, 21, 86, 91	syl21anc 837	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (¬ 𝑆 ≤ 𝑊 ↔ (𝑆 ∧ 𝑊) = (0.‘𝐾)))
93	90, 92	mpbird 257	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ 𝑆 ≤ 𝑊)
94	86, 93	jca 511	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 class class class wbr 5091 I cid 5510 ^◡ccnv 5615 ↾ cres 5618 ∘ ccom 5620 ‘cfv 6481 (class class class)co 7346 Basecbs 17117 lecple 17165 joincjn 18214 meetcmee 18215 0.cp0 18324 OLcol 39212 Atomscatm 39301 HLchlt 39388 LLinesclln 39529 LHypclh 40022 LTrncltrn 40139 trLctrl 40196

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-riotaBAD 38991

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-id 5511 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-1st 7921 df-2nd 7922 df-undef 8203 df-map 8752 df-proset 18197 df-poset 18216 df-plt 18231 df-lub 18247 df-glb 18248 df-join 18249 df-meet 18250 df-p0 18326 df-p1 18327 df-lat 18335 df-clat 18402 df-oposet 39214 df-ol 39216 df-oml 39217 df-covers 39304 df-ats 39305 df-atl 39336 df-cvlat 39360 df-hlat 39389 df-llines 39536 df-lplanes 39537 df-lvols 39538 df-lines 39539 df-psubsp 39541 df-pmap 39542 df-padd 39834 df-lhyp 40026 df-laut 40027 df-ldil 40142 df-ltrn 40143 df-trl 40197

This theorem is referenced by: cdlemi 40858 cdlemki 40879 cdlemksv2 40885 cdlemk16a 40894

W3C validator