cdlemkid1 - Mathbox for Norm Megill

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

Theorem cdlemkid1 41728

Description: Lemma for cdlemkid 41742. (Contributed by NM, 24-Jul-2013.)

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

**Assertion**
Ref	Expression
cdlemkid1	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))

**Proof of Theorem cdlemkid1**
Step	Hyp	Ref	Expression
1		cdlemk5.z	. . 3 ⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))
2	1	oveq1i 7426	. 2 ⊢ (𝑍 ∨ (𝑅‘𝑏)) = (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏))
3		simp1l 1216	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ HL)
4		simp1 1154	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
5		simp3rl 1265	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ∈ 𝑇)
6		simp3rr 1266	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ≠ ( I ↾ 𝐵))
7		cdlemk5.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
8		cdlemk5.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
9		cdlemk5.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
10		cdlemk5.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
11		cdlemk5.r	. . . . . 6 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
12	7, 8, 9, 10, 11	trlnidat 40979	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)) → (𝑅‘𝑏) ∈ 𝐴)
13	4, 5, 6, 12	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐴)
14		simp3ll 1263	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐴)
15		cdlemk5.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
16	7, 15, 8	hlatjcl 40173	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵)
17	3, 14, 13, 16	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵)
18	3	hllatd 40170	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ Lat)
19		simp22 1226	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑁 ∈ 𝑇)
20	7, 8	atbase 40095	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
21	14, 20	syl 18	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐵)
22	7, 9, 10	ltrncl 40931	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑁‘𝑃) ∈ 𝐵)
23	4, 19, 21, 22	syl3anc 1398	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑁‘𝑃) ∈ 𝐵)
24		simp21 1225	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐹 ∈ 𝑇)
25	9, 10	ltrncnv 40952	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
26	4, 24, 25	syl2anc 596	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ^◡𝐹 ∈ 𝑇)
27	9, 10	ltrnco 41525	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝑏 ∘ ^◡𝐹) ∈ 𝑇)
28	4, 5, 26, 27	syl3anc 1398	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑏 ∘ ^◡𝐹) ∈ 𝑇)
29	7, 9, 10, 11	trlcl 40970	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑏 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵)
30	4, 28, 29	syl2anc 596	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵)
31	7, 15	latjcl 18505	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵)
32	18, 23, 30, 31	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵)
33		cdlemk5.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
34	33, 15, 8	hlatlej2 40182	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏)))
35	3, 14, 13, 34	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏)))
36		cdlemk5.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
37	7, 33, 15, 36, 8	atmod2i1 40667	. . . 4 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝑏) ∈ 𝐴 ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵) ∧ (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
38	3, 13, 17, 32, 35, 37	syl131anc 1410	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
39	7, 8	atbase 40095	. . . . . . . 8 ⊢ ((𝑅‘𝑏) ∈ 𝐴 → (𝑅‘𝑏) ∈ 𝐵)
40	13, 39	syl 18	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐵)
41	7, 9, 10, 11	trlcl 40970	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑅‘𝑁) ∈ 𝐵)
42	4, 19, 41	syl2anc 596	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑁) ∈ 𝐵)
43	7, 15	latj32 18551	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵)) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
44	18, 21, 40, 42, 43	syl13anc 1399	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
45		simp3l 1220	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
46	33, 15, 8, 9, 10, 11	trljat3 40974	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁)))
47	4, 19, 45, 46	syl3anc 1398	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁)))
48	47	oveq1d 7431	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
49	7, 15	latjass 18549	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
50	18, 23, 42, 40, 49	syl13anc 1399	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
51	44, 48, 50	3eqtrd 2805	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
52	7, 15	latjass 18549	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
53	18, 23, 30, 40, 52	syl13anc 1399	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
54	7, 15	latjcom 18513	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
55	18, 42, 40, 54	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
56	9, 10, 11	trlcnv 40971	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
57	4, 24, 56	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
58		simp23 1227	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝐹) = (𝑅‘𝑁))
59	57, 58	eqtrd 2801	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘^◡𝐹) = (𝑅‘𝑁))
60	59	oveq2d 7432	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
61	55, 60	eqtr4d 2804	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
62	15, 9, 10, 11	trljco 41546	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
63	4, 5, 26, 62	syl3anc 1398	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
64	7, 15	latjcom 18513	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
65	18, 40, 30, 64	syl3anc 1398	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
66	61, 63, 65	3eqtr2d 2807	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
67	66	oveq2d 7432	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
68	53, 67	eqtr4d 2804	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
69	51, 68	eqtr4d 2804	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)))
70	69	oveq2d 7432	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
71	7, 15, 36	latabs2 18542	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏)))
72	18, 17, 42, 71	syl3anc 1398	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏)))
73	38, 70, 72	3eqtr2d 2807	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))
74	2, 73	eqtrid 2813	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 class class class wbr 5112 I cid 5558 ^◡ccnv 5663 ↾ cres 5666 ∘ ccom 5668 ‘cfv 6540 (class class class)co 7416 Basecbs 17279 lecple 17327 joincjn 18377 meetcmee 18378 Latclat 18497 Atomscatm 40069 HLchlt 40156 LHypclh 40790 LTrncltrn 40907 trLctrl 40964

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5241 ax-sep 5260 ax-nul 5272 ax-pow 5339 ax-pr 5407 ax-un 7738 ax-riotaBAD 39759

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4876 df-iun 4961 df-iin 4962 df-br 5113 df-opab 5177 df-mpt 5196 df-id 5559 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-1st 7988 df-2nd 7989 df-undef 8271 df-map 8828 df-proset 18360 df-poset 18379 df-plt 18394 df-lub 18410 df-glb 18411 df-join 18412 df-meet 18413 df-p0 18489 df-p1 18490 df-lat 18498 df-clat 18565 df-oposet 39982 df-ol 39984 df-oml 39985 df-covers 40072 df-ats 40073 df-atl 40104 df-cvlat 40128 df-hlat 40157 df-llines 40304 df-lplanes 40305 df-lvols 40306 df-lines 40307 df-psubsp 40309 df-pmap 40310 df-padd 40602 df-lhyp 40794 df-laut 40795 df-ldil 40910 df-ltrn 40911 df-trl 40965

This theorem is used by: cdlemkid2 41730

W3C validator