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 41546

Description: Lemma for cdlemkid 41560. (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 7406	. 2 ⊢ (𝑍 ∨ (𝑅‘𝑏)) = (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏))
3		simp1l 1211	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ HL)
4		simp1 1149	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
5		simp3rl 1260	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ∈ 𝑇)
6		simp3rr 1261	. . . . 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 40797	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)) → (𝑅‘𝑏) ∈ 𝐴)
13	4, 5, 6, 12	syl3anc 1390	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐴)
14		simp3ll 1258	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐴)
15		cdlemk5.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
16	7, 15, 8	hlatjcl 39991	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵)
17	3, 14, 13, 16	syl3anc 1390	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵)
18	3	hllatd 39988	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ Lat)
19		simp22 1221	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑁 ∈ 𝑇)
20	7, 8	atbase 39913	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
21	14, 20	syl 17	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐵)
22	7, 9, 10	ltrncl 40749	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → (𝑁‘𝑃) ∈ 𝐵)
23	4, 19, 21, 22	syl3anc 1390	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑁‘𝑃) ∈ 𝐵)
24		simp21 1220	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐹 ∈ 𝑇)
25	9, 10	ltrncnv 40770	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
26	4, 24, 25	syl2anc 593	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ^◡𝐹 ∈ 𝑇)
27	9, 10	ltrnco 41343	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝑏 ∘ ^◡𝐹) ∈ 𝑇)
28	4, 5, 26, 27	syl3anc 1390	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑏 ∘ ^◡𝐹) ∈ 𝑇)
29	7, 9, 10, 11	trlcl 40788	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑏 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵)
30	4, 28, 29	syl2anc 593	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵)
31	7, 15	latjcl 18471	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵)
32	18, 23, 30, 31	syl3anc 1390	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵)
33		cdlemk5.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
34	33, 15, 8	hlatlej2 40000	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝑏) ∈ 𝐴) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏)))
35	3, 14, 13, 34	syl3anc 1390	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏)))
36		cdlemk5.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
37	7, 33, 15, 36, 8	atmod2i1 40485	. . . 4 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝑏) ∈ 𝐴 ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∈ 𝐵) ∧ (𝑅‘𝑏) ≤ (𝑃 ∨ (𝑅‘𝑏))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
38	3, 13, 17, 32, 35, 37	syl131anc 1402	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
39	7, 8	atbase 39913	. . . . . . . 8 ⊢ ((𝑅‘𝑏) ∈ 𝐴 → (𝑅‘𝑏) ∈ 𝐵)
40	13, 39	syl 17	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐵)
41	7, 9, 10, 11	trlcl 40788	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑅‘𝑁) ∈ 𝐵)
42	4, 19, 41	syl2anc 593	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑁) ∈ 𝐵)
43	7, 15	latj32 18517	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵)) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
44	18, 21, 40, 42, 43	syl13anc 1391	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
45		simp3l 1215	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
46	33, 15, 8, 9, 10, 11	trljat3 40792	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁)))
47	4, 19, 45, 46	syl3anc 1390	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ (𝑅‘𝑁)))
48	47	oveq1d 7411	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)))
49	7, 15	latjass 18515	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
50	18, 23, 42, 40, 49	syl13anc 1391	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘𝑁)) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
51	44, 48, 50	3eqtrd 2801	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
52	7, 15	latjass 18515	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ ((𝑁‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵)) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
53	18, 23, 30, 40, 52	syl13anc 1391	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
54	7, 15	latjcom 18479	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑁) ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
55	18, 42, 40, 54	syl3anc 1390	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
56	9, 10, 11	trlcnv 40789	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
57	4, 24, 56	syl2anc 593	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘^◡𝐹) = (𝑅‘𝐹))
58		simp23 1222	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝐹) = (𝑅‘𝑁))
59	57, 58	eqtrd 2797	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘^◡𝐹) = (𝑅‘𝑁))
60	59	oveq2d 7412	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)) = ((𝑅‘𝑏) ∨ (𝑅‘𝑁)))
61	55, 60	eqtr4d 2800	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
62	15, 9, 10, 11	trljco 41364	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
63	4, 5, 26, 62	syl3anc 1390	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘𝑏) ∨ (𝑅‘^◡𝐹)))
64	7, 15	latjcom 18479	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑅‘𝑏) ∈ 𝐵 ∧ (𝑅‘(𝑏 ∘ ^◡𝐹)) ∈ 𝐵) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
65	18, 40, 30, 64	syl3anc 1390	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑏) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
66	61, 63, 65	3eqtr2d 2803	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅‘𝑁) ∨ (𝑅‘𝑏)) = ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏)))
67	66	oveq2d 7412	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))) = ((𝑁‘𝑃) ∨ ((𝑅‘(𝑏 ∘ ^◡𝐹)) ∨ (𝑅‘𝑏))))
68	53, 67	eqtr4d 2800	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)) = ((𝑁‘𝑃) ∨ ((𝑅‘𝑁) ∨ (𝑅‘𝑏))))
69	51, 68	eqtr4d 2800	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁)) = (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏)))
70	69	oveq2d 7412	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = ((𝑃 ∨ (𝑅‘𝑏)) ∧ (((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))) ∨ (𝑅‘𝑏))))
71	7, 15, 36	latabs2 18508	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝑅‘𝑏)) ∈ 𝐵 ∧ (𝑅‘𝑁) ∈ 𝐵) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏)))
72	18, 17, 42, 71	syl3anc 1390	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑃 ∨ (𝑅‘𝑏)) ∨ (𝑅‘𝑁))) = (𝑃 ∨ (𝑅‘𝑏)))
73	38, 70, 72	3eqtr2d 2803	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹)))) ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))
74	2, 73	eqtrid 2809	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 ≠ wne 2957 class class class wbr 5100 I cid 5541 ^◡ccnv 5646 ↾ cres 5649 ∘ ccom 5651 ‘cfv 6521 (class class class)co 7396 Basecbs 17245 lecple 17293 joincjn 18343 meetcmee 18344 Latclat 18463 Atomscatm 39887 HLchlt 39974 LHypclh 40608 LTrncltrn 40725 trLctrl 40782

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-riotaBAD 39577

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5542 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-1st 7970 df-2nd 7971 df-undef 8253 df-map 8810 df-proset 18326 df-poset 18345 df-plt 18360 df-lub 18376 df-glb 18377 df-join 18378 df-meet 18379 df-p0 18455 df-p1 18456 df-lat 18464 df-clat 18531 df-oposet 39800 df-ol 39802 df-oml 39803 df-covers 39890 df-ats 39891 df-atl 39922 df-cvlat 39946 df-hlat 39975 df-llines 40122 df-lplanes 40123 df-lvols 40124 df-lines 40125 df-psubsp 40127 df-pmap 40128 df-padd 40420 df-lhyp 40612 df-laut 40613 df-ldil 40728 df-ltrn 40729 df-trl 40783

This theorem is referenced by: cdlemkid2 41548

W3C validator