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 40940

Description: Lemma for cdlemkid 40954. (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 7351	. 2 ⊢ (𝑍 ∨ (𝑅‘𝑏)) = (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏))
3		simp1l 1198	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ HL)
4		simp1 1136	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
5		simp3rl 1247	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ∈ 𝑇)
6		simp3rr 1248	. . . . 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 40191	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)) → (𝑅‘𝑏) ∈ 𝐴)
13	4, 5, 6, 12	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐴)
14		simp3ll 1245	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐴)
15		cdlemk5.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
16	7, 15, 8	hlatjcl 39385	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵)
17	3, 14, 13, 16	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵)
18	3	hllatd 39382	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ Lat)
19		simp22 1208	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑁 ∈ 𝑇)
20	7, 8	atbase 39307	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
21	14, 20	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐵)
22	7, 9, 10	ltrncl 40143	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑁‘𝑃) ∈ 𝐵)
23	4, 19, 21, 22	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑁‘𝑃) ∈ 𝐵)
24		simp21 1207	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐹 ∈ 𝑇)
25	9, 10	ltrncnv 40164	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
26	4, 24, 25	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ^◡𝐹 ∈ 𝑇)
27	9, 10	ltrnco 40737	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝑏 ∘ ^◡𝐹) ∈ 𝑇)
28	4, 5, 26, 27	syl3anc 1373	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑏 ∘ ^◡𝐹) ∈ 𝑇)
29	7, 9, 10, 11	trlcl 40182	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑏 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵)
30	4, 28, 29	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵)
31	7, 15	latjcl 18337	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵)
32	18, 23, 30, 31	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵)
33		cdlemk5.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
34	33, 15, 8	hlatlej2 39394	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏)))
35	3, 14, 13, 34	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏)))
36		cdlemk5.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
37	7, 33, 15, 36, 8	atmod2i1 39879	. . . 4 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝑏) ∈ 𝐴 ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵) ∧ (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
38	3, 13, 17, 32, 35, 37	syl131anc 1385	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
39	7, 8	atbase 39307	. . . . . . . 8 ⊢ ((𝑅‘𝑏) ∈ 𝐴 → (𝑅‘𝑏) ∈ 𝐵)
40	13, 39	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐵)
41	7, 9, 10, 11	trlcl 40182	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑅‘𝑁) ∈ 𝐵)
42	4, 19, 41	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑁) ∈ 𝐵)
43	7, 15	latj32 18383	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵)) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
44	18, 21, 40, 42, 43	syl13anc 1374	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
45		simp3l 1202	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
46	33, 15, 8, 9, 10, 11	trljat3 40186	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁)))
47	4, 19, 45, 46	syl3anc 1373	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁)))
48	47	oveq1d 7356	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
49	7, 15	latjass 18381	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
50	18, 23, 42, 40, 49	syl13anc 1374	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
51	44, 48, 50	3eqtrd 2769	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
52	7, 15	latjass 18381	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
53	18, 23, 30, 40, 52	syl13anc 1374	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
54	7, 15	latjcom 18345	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
55	18, 42, 40, 54	syl3anc 1373	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
56	9, 10, 11	trlcnv 40183	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
57	4, 24, 56	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
58		simp23 1209	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝐹) = (𝑅‘𝑁))
59	57, 58	eqtrd 2765	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘^◡𝐹) = (𝑅‘𝑁))
60	59	oveq2d 7357	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
61	55, 60	eqtr4d 2768	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
62	15, 9, 10, 11	trljco 40758	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
63	4, 5, 26, 62	syl3anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
64	7, 15	latjcom 18345	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
65	18, 40, 30, 64	syl3anc 1373	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
66	61, 63, 65	3eqtr2d 2771	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
67	66	oveq2d 7357	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
68	53, 67	eqtr4d 2768	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
69	51, 68	eqtr4d 2768	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)))
70	69	oveq2d 7357	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
71	7, 15, 36	latabs2 18374	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏)))
72	18, 17, 42, 71	syl3anc 1373	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏)))
73	38, 70, 72	3eqtr2d 2771	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))
74	2, 73	eqtrid 2777	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2110 ≠ wne 2926 class class class wbr 5089 I cid 5508 ^◡ccnv 5613 ↾ cres 5616 ∘ ccom 5618 ‘cfv 6477 (class class class)co 7341 Basecbs 17112 lecple 17160 joincjn 18209 meetcmee 18210 Latclat 18329 Atomscatm 39281 HLchlt 39368 LHypclh 40002 LTrncltrn 40119 trLctrl 40176

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 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-riotaBAD 38971

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 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-iun 4941 df-iin 4942 df-br 5090 df-opab 5152 df-mpt 5171 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-1st 7916 df-2nd 7917 df-undef 8198 df-map 8747 df-proset 18192 df-poset 18211 df-plt 18226 df-lub 18242 df-glb 18243 df-join 18244 df-meet 18245 df-p0 18321 df-p1 18322 df-lat 18330 df-clat 18397 df-oposet 39194 df-ol 39196 df-oml 39197 df-covers 39284 df-ats 39285 df-atl 39316 df-cvlat 39340 df-hlat 39369 df-llines 39516 df-lplanes 39517 df-lvols 39518 df-lines 39519 df-psubsp 39521 df-pmap 39522 df-padd 39814 df-lhyp 40006 df-laut 40007 df-ldil 40122 df-ltrn 40123 df-trl 40177

This theorem is referenced by: cdlemkid2 40942

W3C validator