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 41187

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 1137	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇))
2		simp21l 1292	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐴)
3		simp22l 1294	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ∈ 𝐴)
4		simp23 1210	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹)))
5		simp33 1213	. . . . 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 41185	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
16	1, 2, 3, 4, 5, 15	syl122anc 1382	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
17		oveq1 7375	. . . . . . . 8 ⊢ (𝑆 = (0.‘𝐾) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((0.‘𝐾) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
18		simp11l 1286	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ HL)
19		hlol 39731	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ OL)
21		simp11r 1287	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑊 ∈ 𝐻)
22	18, 21	jca 511	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
23		simp13 1207	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇)
24		simp12 1206	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇)
25	11, 12	ltrncnv 40516	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
26	22, 24, 25	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ∈ 𝑇)
27	23, 26	jca 511	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇))
28	5	necomd 2988	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≠ (𝑅‘𝐹))
29	11, 12, 13	trlcnv 40535	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
30	22, 24, 29	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
31	28, 30	neeqtrrd 3007	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≠ (𝑅‘^◡𝐹))
32	10, 11, 12, 13	trlcoat 41093	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ (𝑅‘𝐺) ≠ (𝑅‘^◡𝐹)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
33	22, 27, 31, 32	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
34	6, 10	atbase 39659	. . . . . . . . . 10 ⊢ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
35	33, 34	syl 17	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
36		eqid 2737	. . . . . . . . . 10 ⊢ (0.‘𝐾) = (0.‘𝐾)
37	6, 8, 36	olj02 39596	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵) → ((0.‘𝐾) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
38	20, 35, 37	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((0.‘𝐾) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
39	17, 38	sylan9eqr 2794	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ 𝑆 = (0.‘𝐾)) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
40	11, 12	ltrnco 41089	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
41	22, 23, 26, 40	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
42	7, 11, 12, 13	trlle 40554	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
43	22, 41, 42	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
44		simp22r 1295	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ 𝑄 ≤ 𝑊)
45		nbrne2 5120	. . . . . . . . . . . . 13 ⊢ (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ 𝑄)
46	45	necomd 2988	. . . . . . . . . . . 12 ⊢ (((𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊 ∧ ¬ 𝑄 ≤ 𝑊) → 𝑄 ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
47	43, 44, 46	syl2anc 585	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
48		eqid 2737	. . . . . . . . . . . 12 ⊢ (LLines‘𝐾) = (LLines‘𝐾)
49	8, 10, 48	llni2 39882	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴) ∧ 𝑄 ≠ (𝑅‘(𝐺 ∘ ^◡𝐹))) → (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ (LLines‘𝐾))
50	18, 3, 33, 47, 49	syl31anc 1376	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ (LLines‘𝐾))
51	10, 48	llnneat 39884	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ (LLines‘𝐾)) → ¬ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐴)
52	18, 50, 51	syl2anc 585	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐴)
53		nelne2 3031	. . . . . . . . 9 ⊢ (((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 ∧ ¬ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐴) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
54	33, 52, 53	syl2anc 585	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
55	54	adantr 480	. . . . . . 7 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ 𝑆 = (0.‘𝐾)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
56	39, 55	eqnetrd 3000	. . . . . 6 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) ∧ 𝑆 = (0.‘𝐾)) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
57	56	ex 412	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 = (0.‘𝐾) → (𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
58	57	necon2d 2956	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑆 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) → 𝑆 ≠ (0.‘𝐾)))
59	16, 58	mpd 15	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑆 ≠ (0.‘𝐾))
60		simp32 1212	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ≠ ( I ↾ 𝐵))
61	6, 10, 11, 12, 13	trlnidat 40543	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ 𝐴)
62	22, 23, 60, 61	syl3anc 1374	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ 𝐴)
63	7, 8, 10	hlatlej2 39746	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)))
64	18, 2, 62, 63	syl3anc 1374	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)))
65		simp22 1209	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
66		simp31 1211	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ≠ ( I ↾ 𝐵))
67	6, 11, 12	ltrncnvnid 40497	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → ^◡𝐹 ≠ ( I ↾ 𝐵))
68	22, 24, 66, 67	syl3anc 1374	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ≠ ( I ↾ 𝐵))
69	6, 11, 12, 13	trlcone 41098	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ ((𝑅‘𝐺) ≠ (𝑅‘^◡𝐹) ∧ ^◡𝐹 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐺) ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
70	69	necomd 2988	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ ((𝑅‘𝐺) ≠ (𝑅‘^◡𝐹) ∧ ^◡𝐹 ≠ ( I ↾ 𝐵))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑅‘𝐺))
71	22, 23, 26, 31, 68, 70	syl122anc 1382	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑅‘𝐺))
72	7, 11, 12, 13	trlle 40554	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ≤ 𝑊)
73	22, 23, 72	syl2anc 585	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≤ 𝑊)
74	7, 8, 10, 11	lhp2atnle 40403	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ≠ (𝑅‘𝐺)) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊) ∧ ((𝑅‘𝐺) ∈ 𝐴 ∧ (𝑅‘𝐺) ≤ 𝑊)) → ¬ (𝑅‘𝐺) ≤ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
75	22, 65, 71, 33, 43, 62, 73, 74	syl322anc 1401	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ¬ (𝑅‘𝐺) ≤ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
76		nbrne1 5119	. . . . . . . 8 ⊢ (((𝑅‘𝐺) ≤ (𝑃 ∨ (𝑅‘𝐺)) ∧ ¬ (𝑅‘𝐺) ≤ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) → (𝑃 ∨ (𝑅‘𝐺)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
77	64, 75, 76	syl2anc 585	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∨ (𝑅‘𝐺)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
78	8, 9, 36, 10	2atmat0 39896	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) ∧ (𝑄 ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 ∧ (𝑃 ∨ (𝑅‘𝐺)) ≠ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾)))
79	18, 2, 62, 3, 33, 77, 78	syl33anc 1388	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾)))
80	14	eleq1i 2828	. . . . . . 7 ⊢ (𝑆 ∈ 𝐴 ↔ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴)
81	14	eqeq1i 2742	. . . . . . 7 ⊢ (𝑆 = (0.‘𝐾) ↔ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾))
82	80, 81	orbi12i 915	. . . . . 6 ⊢ ((𝑆 ∈ 𝐴 ∨ 𝑆 = (0.‘𝐾)) ↔ (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∨ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = (0.‘𝐾)))
83	79, 82	sylibr 234	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∈ 𝐴 ∨ 𝑆 = (0.‘𝐾)))
84	83	ord 865	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (¬ 𝑆 ∈ 𝐴 → 𝑆 = (0.‘𝐾)))
85	84	necon1ad 2950	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ≠ (0.‘𝐾) → 𝑆 ∈ 𝐴))
86	59, 85	mpd 15	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑆 ∈ 𝐴)
87		simp21 1208	. . . . 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 41186	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∧ 𝑊) = (0.‘𝐾))
90	88, 89	syld3an2 1414	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∧ 𝑊) = (0.‘𝐾))
91	7, 9, 36, 10, 11	lhpmatb 40401	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐴) → (¬ 𝑆 ≤ 𝑊 ↔ (𝑆 ∧ 𝑊) = (0.‘𝐾)))
92	18, 21, 86, 91	syl21anc 838	. . 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 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 class class class wbr 5100 I cid 5526 ^◡ccnv 5631 ↾ cres 5634 ∘ ccom 5636 ‘cfv 6500 (class class class)co 7368 Basecbs 17148 lecple 17196 joincjn 18246 meetcmee 18247 0.cp0 18356 OLcol 39544 Atomscatm 39633 HLchlt 39720 LLinesclln 39861 LHypclh 40354 LTrncltrn 40471 trLctrl 40528

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 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-riotaBAD 39323

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 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-1st 7943 df-2nd 7944 df-undef 8225 df-map 8777 df-proset 18229 df-poset 18248 df-plt 18263 df-lub 18279 df-glb 18280 df-join 18281 df-meet 18282 df-p0 18358 df-p1 18359 df-lat 18367 df-clat 18434 df-oposet 39546 df-ol 39548 df-oml 39549 df-covers 39636 df-ats 39637 df-atl 39668 df-cvlat 39692 df-hlat 39721 df-llines 39868 df-lplanes 39869 df-lvols 39870 df-lines 39871 df-psubsp 39873 df-pmap 39874 df-padd 40166 df-lhyp 40358 df-laut 40359 df-ldil 40474 df-ltrn 40475 df-trl 40529

This theorem is referenced by: cdlemi 41190 cdlemki 41211 cdlemksv2 41217 cdlemk16a 41226

W3C validator