cdlemh2 - Mathbox for Norm Megill

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

Theorem cdlemh2 41966

Description: Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-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	⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
cdlemh.z	⊢ 0 = (0.‘𝐾)

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

**Proof of Theorem cdlemh2**
Step	Hyp	Ref	Expression
1		cdlemh.s	. . 3 ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
2	1	oveq1i 7430	. 2 ⊢ (𝑆 ∧ 𝑊) = (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∧ 𝑊)
3		simp11l 1303	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ HL)
4		hlol 40511	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
5	3, 4	syl 18	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ OL)
6	3	hllatd 40514	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ Lat)
7		simp2ll 1259	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐴)
8		cdlemh.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐾)
9		cdlemh.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
10	8, 9	atbase 40439	. . . . . 6 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
11	7, 10	syl 18	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐵)
12		simp11r 1304	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑊 ∈ 𝐻)
13	3, 12	jca 521	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
14		simp13 1224	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇)
15		cdlemh.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
16		cdlemh.t	. . . . . . 7 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
17		cdlemh.r	. . . . . . 7 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
18	8, 15, 16, 17	trlcl 41314	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ 𝐵)
19	13, 14, 18	syl2anc 596	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ 𝐵)
20		cdlemh.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
21	8, 20	latjcl 18618	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ (𝑅‘𝐺) ∈ 𝐵) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
22	6, 11, 19, 21	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
23		simp2rl 1261	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ∈ 𝐴)
24	8, 9	atbase 40439	. . . . . 6 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
25	23, 24	syl 18	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑄 ∈ 𝐵)
26		simp12 1223	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇)
27	15, 16	ltrncnv 41296	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
28	13, 26, 27	syl2anc 596	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ∈ 𝑇)
29	15, 16	ltrnco 41869	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
30	13, 14, 28, 29	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
31	8, 15, 16, 17	trlcl 41314	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
32	13, 30, 31	syl2anc 596	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
33	8, 20	latjcl 18618	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵) → (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
34	6, 25, 32, 33	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
35	8, 15	lhpbase 41148	. . . . 5 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
36	12, 35	syl 18	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑊 ∈ 𝐵)
37		cdlemh.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
38	8, 37	latmassOLD 40379	. . . 4 ⊢ ((𝐾 ∈ OL ∧ ((𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵 ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∧ 𝑊) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∧ 𝑊)))
39	5, 22, 34, 36, 38	syl13anc 1399	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∧ 𝑊) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∧ 𝑊)))
40		simp2r 1219	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
41		cdlemh.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
42		cdlemh.z	. . . . . . . 8 ⊢ 0 = (0.‘𝐾)
43	41, 37, 42, 9, 15	lhpmat 41180	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑄 ∧ 𝑊) = 0 )
44	13, 40, 43	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑄 ∧ 𝑊) = 0 )
45	44	oveq1d 7435	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑄 ∧ 𝑊) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ( 0 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
46	41, 15, 16, 17	trlle 41334	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
47	13, 30, 46	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)
48	8, 41, 20, 37, 9	atmod4i2 41017	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊) → ((𝑄 ∧ 𝑊) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∧ 𝑊))
49	3, 23, 32, 36, 47, 48	syl131anc 1410	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑄 ∧ 𝑊) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∧ 𝑊))
50	8, 20, 42	olj02 40376	. . . . . 6 ⊢ ((𝐾 ∈ OL ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵) → ( 0 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
51	5, 32, 50	syl2anc 596	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ( 0 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) = (𝑅‘(𝐺 ∘ ^◡𝐹)))
52	45, 49, 51	3eqtr3rd 2804	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) = ((𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∧ 𝑊))
53	52	oveq2d 7436	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑅‘(𝐺 ∘ ^◡𝐹))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∧ 𝑊)))
54		simp2l 1218	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
55	14, 28	jca 521	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇))
56		simp33 1230	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐹) ≠ (𝑅‘𝐺))
57	56	necomd 3010	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≠ (𝑅‘𝐹))
58	15, 16, 17	trlcnv 41315	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
59	13, 26, 58	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
60	57, 59	neeqtrrd 3029	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≠ (𝑅‘^◡𝐹))
61		simp31 1228	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ≠ ( I ↾ 𝐵))
62	8, 15, 16	ltrncnvnid 41277	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) → ^◡𝐹 ≠ ( I ↾ 𝐵))
63	13, 26, 61, 62	syl3anc 1398	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ≠ ( I ↾ 𝐵))
64	8, 15, 16, 17	trlcone 41878	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ ((𝑅‘𝐺) ≠ (𝑅‘^◡𝐹) ∧ ^◡𝐹 ≠ ( I ↾ 𝐵))) → (𝑅‘𝐺) ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
65	13, 55, 60, 63, 64	syl112anc 1401	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≠ (𝑅‘(𝐺 ∘ ^◡𝐹)))
66		simp32 1229	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ≠ ( I ↾ 𝐵))
67	8, 9, 15, 16, 17	trlnidat 41323	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) → (𝑅‘𝐺) ∈ 𝐴)
68	13, 14, 66, 67	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ 𝐴)
69	41, 15, 16, 17	trlle 41334	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ≤ 𝑊)
70	13, 14, 69	syl2anc 596	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ≤ 𝑊)
71	9, 15, 16, 17	trlcoat 41873	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) ∧ (𝑅‘𝐺) ≠ (𝑅‘^◡𝐹)) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
72	13, 55, 60, 71	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴)
73	41, 20, 37, 42, 9, 15	lhp2at0 41182	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐺) ≠ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∧ ((𝑅‘𝐺) ∈ 𝐴 ∧ (𝑅‘𝐺) ≤ 𝑊) ∧ ((𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐴 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ≤ 𝑊)) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑅‘(𝐺 ∘ ^◡𝐹))) = 0 )
74	13, 54, 65, 68, 70, 72, 47, 73	syl322anc 1425	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑅‘(𝐺 ∘ ^◡𝐹))) = 0 )
75	39, 53, 74	3eqtr2rd 2802	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 0 = (((𝑃 ∨ (𝑅‘𝐺)) ∧ (𝑄 ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∧ 𝑊))
76	2, 75	eqtr4id 2814	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑆 ∧ 𝑊) = 0 )

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 I cid 5544 ^◡ccnv 5649 ↾ cres 5652 ∘ ccom 5654 ‘cfv 6538 (class class class)co 7420 Basecbs 17392 lecple 17440 joincjn 18490 meetcmee 18491 0.cp0 18600 Latclat 18610 OLcol 40324 Atomscatm 40413 HLchlt 40500 LHypclh 41134 LTrncltrn 41251 trLctrl 41308

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-riotaBAD 40103

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-undef 8293 df-map 8852 df-proset 18473 df-poset 18492 df-plt 18507 df-lub 18523 df-glb 18524 df-join 18525 df-meet 18526 df-p0 18602 df-p1 18603 df-lat 18611 df-clat 18678 df-oposet 40326 df-ol 40328 df-oml 40329 df-covers 40416 df-ats 40417 df-atl 40448 df-cvlat 40472 df-hlat 40501 df-llines 40648 df-lplanes 40649 df-lvols 40650 df-lines 40651 df-psubsp 40653 df-pmap 40654 df-padd 40946 df-lhyp 41138 df-laut 41139 df-ldil 41254 df-ltrn 41255 df-trl 41309

This theorem is used by: cdlemh 41967

W3C validator