cdlemg10a - Mathbox for Norm Megill

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

Theorem cdlemg10a 40619

Description: TODO: FIX COMMENT. (Contributed by NM, 3-May-2013.)

**Hypotheses**
Ref	Expression
cdlemg8.l	⊢ ≤ = (le‘𝐾)
cdlemg8.j	⊢ ∨ = (join‘𝐾)
cdlemg8.m	⊢ ∧ = (meet‘𝐾)
cdlemg8.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemg8.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemg8.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemg10.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

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

**Proof of Theorem cdlemg10a**
Step	Hyp	Ref	Expression
1		simp11 1204	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		simp12 1205	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
3		simp13 1206	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
4		simp21 1207	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝐹 ∈ 𝑇)
5		simp22 1208	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝐺 ∈ 𝑇)
6		simp23 1209	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝑃 ≠ 𝑄)
7		simp31 1210	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))
8		cdlemg8.l	. . . 4 ⊢ ≤ = (le‘𝐾)
9		cdlemg8.j	. . . 4 ⊢ ∨ = (join‘𝐾)
10		cdlemg8.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
11		cdlemg8.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
12		cdlemg8.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
13		cdlemg8.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
14	8, 9, 10, 11, 12, 13	cdlemg9 40613	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝐹 ∈ 𝑇) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)) ∧ ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄))) ∨ (((𝐺‘𝑃) ∨ 𝑃) ∧ ((𝐺‘𝑄) ∨ 𝑄))))
15	1, 2, 3, 4, 5, 6, 7, 14	syl133anc 1395	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)) ∧ ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄))) ∨ (((𝐺‘𝑃) ∨ 𝑃) ∧ ((𝐺‘𝑄) ∨ 𝑄))))
16	8, 11, 12, 13	ltrnel 40118	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐺‘𝑃) ∈ 𝐴 ∧ ¬ (𝐺‘𝑃) ≤ 𝑊))
17	1, 5, 2, 16	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝐺‘𝑃) ∈ 𝐴 ∧ ¬ (𝐺‘𝑃) ≤ 𝑊))
18	8, 11, 12, 13	ltrnel 40118	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐺‘𝑄) ∈ 𝐴 ∧ ¬ (𝐺‘𝑄) ≤ 𝑊))
19	1, 5, 3, 18	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝐺‘𝑄) ∈ 𝐴 ∧ ¬ (𝐺‘𝑄) ≤ 𝑊))
20		simp12l 1287	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝑃 ∈ 𝐴)
21		simp13l 1289	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝑄 ∈ 𝐴)
22	11, 12, 13	ltrn11at 40126	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → (𝐺‘𝑃) ≠ (𝐺‘𝑄))
23	1, 5, 20, 21, 6, 22	syl113anc 1384	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝐺‘𝑃) ≠ (𝐺‘𝑄))
24		simp32 1211	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄))
25		cdlemg10.r	. . . . . . . 8 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
26	8, 9, 10, 11, 12, 13, 25	cdlemg10c 40618	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇)) → ((𝑅‘𝐹) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)) ↔ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄)))
27	1, 2, 3, 4, 5, 26	syl122anc 1381	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑅‘𝐹) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)) ↔ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄)))
28	24, 27	mtbird 325	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ¬ (𝑅‘𝐹) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))
29	8, 9, 10, 11, 12, 13, 25	trlval4 40167	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ ((𝐺‘𝑃) ∈ 𝐴 ∧ ¬ (𝐺‘𝑃) ≤ 𝑊) ∧ ((𝐺‘𝑄) ∈ 𝐴 ∧ ¬ (𝐺‘𝑄) ≤ 𝑊)) ∧ ((𝐺‘𝑃) ≠ (𝐺‘𝑄) ∧ ¬ (𝑅‘𝐹) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))) → (𝑅‘𝐹) = (((𝐺‘𝑃) ∨ (𝐹‘(𝐺‘𝑃))) ∧ ((𝐺‘𝑄) ∨ (𝐹‘(𝐺‘𝑄)))))
30	1, 4, 17, 19, 23, 28, 29	syl132anc 1390	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑅‘𝐹) = (((𝐺‘𝑃) ∨ (𝐹‘(𝐺‘𝑃))) ∧ ((𝐺‘𝑄) ∨ (𝐹‘(𝐺‘𝑄)))))
31		simp11l 1285	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝐾 ∈ HL)
32	8, 11, 12, 13	ltrnat 40119	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → (𝐺‘𝑃) ∈ 𝐴)
33	1, 5, 20, 32	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝐺‘𝑃) ∈ 𝐴)
34	8, 11, 12, 13	ltrnat 40119	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝐺‘𝑃) ∈ 𝐴) → (𝐹‘(𝐺‘𝑃)) ∈ 𝐴)
35	1, 4, 33, 34	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝐹‘(𝐺‘𝑃)) ∈ 𝐴)
36	9, 11	hlatjcom 39346	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝐺‘𝑃) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑃)) ∈ 𝐴) → ((𝐺‘𝑃) ∨ (𝐹‘(𝐺‘𝑃))) = ((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)))
37	31, 33, 35, 36	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝐺‘𝑃) ∨ (𝐹‘(𝐺‘𝑃))) = ((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)))
38	8, 11, 12, 13	ltrnat 40119	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑄 ∈ 𝐴) → (𝐺‘𝑄) ∈ 𝐴)
39	1, 5, 21, 38	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝐺‘𝑄) ∈ 𝐴)
40	8, 11, 12, 13	ltrnat 40119	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝐺‘𝑄) ∈ 𝐴) → (𝐹‘(𝐺‘𝑄)) ∈ 𝐴)
41	1, 4, 39, 40	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝐹‘(𝐺‘𝑄)) ∈ 𝐴)
42	9, 11	hlatjcom 39346	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝐺‘𝑄) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑄)) ∈ 𝐴) → ((𝐺‘𝑄) ∨ (𝐹‘(𝐺‘𝑄))) = ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄)))
43	31, 39, 41, 42	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝐺‘𝑄) ∨ (𝐹‘(𝐺‘𝑄))) = ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄)))
44	37, 43	oveq12d 7371	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (((𝐺‘𝑃) ∨ (𝐹‘(𝐺‘𝑃))) ∧ ((𝐺‘𝑄) ∨ (𝐹‘(𝐺‘𝑄)))) = (((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)) ∧ ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄))))
45	30, 44	eqtrd 2764	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑅‘𝐹) = (((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)) ∧ ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄))))
46		simp33 1212	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))
47	8, 9, 10, 11, 12, 13, 25	trlval4 40167	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ (𝑄 ∨ (𝐺‘𝑄))))
48	1, 5, 2, 3, 6, 46, 47	syl132anc 1390	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ (𝑄 ∨ (𝐺‘𝑄))))
49	9, 11	hlatjcom 39346	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐺‘𝑃) ∈ 𝐴) → (𝑃 ∨ (𝐺‘𝑃)) = ((𝐺‘𝑃) ∨ 𝑃))
50	31, 20, 33, 49	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∨ (𝐺‘𝑃)) = ((𝐺‘𝑃) ∨ 𝑃))
51	9, 11	hlatjcom 39346	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ (𝐺‘𝑄) ∈ 𝐴) → (𝑄 ∨ (𝐺‘𝑄)) = ((𝐺‘𝑄) ∨ 𝑄))
52	31, 21, 39, 51	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑄 ∨ (𝐺‘𝑄)) = ((𝐺‘𝑄) ∨ 𝑄))
53	50, 52	oveq12d 7371	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ (𝑄 ∨ (𝐺‘𝑄))) = (((𝐺‘𝑃) ∨ 𝑃) ∧ ((𝐺‘𝑄) ∨ 𝑄)))
54	48, 53	eqtrd 2764	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑅‘𝐺) = (((𝐺‘𝑃) ∨ 𝑃) ∧ ((𝐺‘𝑄) ∨ 𝑄)))
55	45, 54	oveq12d 7371	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑅‘𝐹) ∨ (𝑅‘𝐺)) = ((((𝐹‘(𝐺‘𝑃)) ∨ (𝐺‘𝑃)) ∧ ((𝐹‘(𝐺‘𝑄)) ∨ (𝐺‘𝑄))) ∨ (((𝐺‘𝑃) ∨ 𝑃) ∧ ((𝐺‘𝑄) ∨ 𝑄))))
56	15, 55	breqtrrd 5123	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄) ∧ (((𝐹‘(𝐺‘𝑃)) ∨ (𝐹‘(𝐺‘𝑄))) ≠ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐹) ≤ (𝑃 ∨ 𝑄) ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ (𝐹‘(𝐺‘𝑃))) ∧ (𝑄 ∨ (𝐹‘(𝐺‘𝑄)))) ≤ ((𝑅‘𝐹) ∨ (𝑅‘𝐺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5095 ‘cfv 6486 (class class class)co 7353 lecple 17186 joincjn 18235 meetcmee 18236 Atomscatm 39241 HLchlt 39328 LHypclh 39963 LTrncltrn 40080 trLctrl 40137

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 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-riotaBAD 38931

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-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4862 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-id 5518 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-1st 7931 df-2nd 7932 df-undef 8213 df-map 8762 df-proset 18218 df-poset 18237 df-plt 18252 df-lub 18268 df-glb 18269 df-join 18270 df-meet 18271 df-p0 18347 df-p1 18348 df-lat 18356 df-clat 18423 df-oposet 39154 df-ol 39156 df-oml 39157 df-covers 39244 df-ats 39245 df-atl 39276 df-cvlat 39300 df-hlat 39329 df-llines 39477 df-lplanes 39478 df-lvols 39479 df-lines 39480 df-psubsp 39482 df-pmap 39483 df-padd 39775 df-lhyp 39967 df-laut 39968 df-ldil 40083 df-ltrn 40084 df-trl 40138

This theorem is referenced by: cdlemg10 40620

W3C validator