Theorem dia2dimlem3 41031

Description: Lemma for dia2dim 41042. Define a translation 𝐷 whose trace is atom 𝑉. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.)

Hypotheses

Ref	Expression
dia2dimlem3.l	⊢ ≤ = (le‘𝐾)
dia2dimlem3.j	⊢ ∨ = (join‘𝐾)
dia2dimlem3.m	⊢ ∧ = (meet‘𝐾)
dia2dimlem3.a	⊢ 𝐴 = (Atoms‘𝐾)
dia2dimlem3.h	⊢ 𝐻 = (LHyp‘𝐾)
dia2dimlem3.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
dia2dimlem3.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
dia2dimlem3.q	⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))
dia2dimlem3.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dia2dimlem3.u	⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
dia2dimlem3.v	⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
dia2dimlem3.p	⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
dia2dimlem3.f	⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
dia2dimlem3.rf	⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
dia2dimlem3.uv	⊢ (𝜑 → 𝑈 ≠ 𝑉)
dia2dimlem3.ru	⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)
dia2dimlem3.rv	⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)
dia2dimlem3.d	⊢ (𝜑 → 𝐷 ∈ 𝑇)
dia2dimlem3.dv	⊢ (𝜑 → (𝐷‘𝑄) = (𝐹‘𝑃))

Assertion

Ref	Expression
dia2dimlem3	⊢ (𝜑 → (𝑅‘𝐷) = 𝑉)

Proof of Theorem dia2dimlem3

Step	Hyp	Ref	Expression
1		dia2dimlem3.k	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2	1	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ HL)
3		dia2dimlem3.f	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
4	3	simpld 494	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
5		dia2dimlem3.p	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
6		dia2dimlem3.l	. . . . . . . . 9 ⊢ ≤ = (le‘𝐾)
7		dia2dimlem3.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
8		dia2dimlem3.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
9		dia2dimlem3.t	. . . . . . . . 9 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
10	6, 7, 8, 9	ltrnel 40104	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
11	1, 4, 5, 10	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
12	11	simpld 494	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑃) ∈ 𝐴)
13		dia2dimlem3.v	. . . . . . 7 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
14	13	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
15		dia2dimlem3.j	. . . . . . 7 ⊢ ∨ = (join‘𝐾)
16	6, 15, 7	hlatlej2 39340	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → 𝑉 ≤ ((𝐹‘𝑃) ∨ 𝑉))
17	2, 12, 14, 16	syl3anc 1373	. . . . 5 ⊢ (𝜑 → 𝑉 ≤ ((𝐹‘𝑃) ∨ 𝑉))
18	2	hllatd 39328	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ Lat)
19		eqid 2735	. . . . . . . 8 ⊢ (Base‘𝐾) = (Base‘𝐾)
20	19, 7	atbase 39253	. . . . . . 7 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
21	14, 20	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
22	19, 15, 7	hlatjcl 39331	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾))
23	2, 12, 14, 22	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾))
24		dia2dimlem3.r	. . . . . . . . 9 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
25	6, 7, 8, 9, 24	trlat 40134	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ∈ 𝐴)
26	1, 5, 3, 25	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑅‘𝐹) ∈ 𝐴)
27		dia2dimlem3.u	. . . . . . . 8 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
28	27	simpld 494	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
29	19, 15, 7	hlatjcl 39331	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑅‘𝐹) ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → ((𝑅‘𝐹) ∨ 𝑈) ∈ (Base‘𝐾))
30	2, 26, 28, 29	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → ((𝑅‘𝐹) ∨ 𝑈) ∈ (Base‘𝐾))
31		dia2dimlem3.m	. . . . . . 7 ⊢ ∧ = (meet‘𝐾)
32	19, 6, 31	latmlem2 18478	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾) ∧ ((𝑅‘𝐹) ∨ 𝑈) ∈ (Base‘𝐾))) → (𝑉 ≤ ((𝐹‘𝑃) ∨ 𝑉) → (((𝑅‘𝐹) ∨ 𝑈) ∧ 𝑉) ≤ (((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))))
33	18, 21, 23, 30, 32	syl13anc 1374	. . . . 5 ⊢ (𝜑 → (𝑉 ≤ ((𝐹‘𝑃) ∨ 𝑉) → (((𝑅‘𝐹) ∨ 𝑈) ∧ 𝑉) ≤ (((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))))
34	17, 33	mpd 15	. . . 4 ⊢ (𝜑 → (((𝑅‘𝐹) ∨ 𝑈) ∧ 𝑉) ≤ (((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
35		dia2dimlem3.rf	. . . . . . 7 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
36	15, 7	hlatjcom 39332	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (𝑈 ∨ 𝑉) = (𝑉 ∨ 𝑈))
37	2, 28, 14, 36	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∨ 𝑉) = (𝑉 ∨ 𝑈))
38	35, 37	breqtrd 5145	. . . . . 6 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑉 ∨ 𝑈))
39		dia2dimlem3.ru	. . . . . . 7 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)
40	6, 15, 7	hlatexch2 39361	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝐹) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑅‘𝐹) ≠ 𝑈) → ((𝑅‘𝐹) ≤ (𝑉 ∨ 𝑈) → 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈)))
41	2, 26, 14, 28, 39, 40	syl131anc 1385	. . . . . 6 ⊢ (𝜑 → ((𝑅‘𝐹) ≤ (𝑉 ∨ 𝑈) → 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈)))
42	38, 41	mpd 15	. . . . 5 ⊢ (𝜑 → 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈))
43	19, 6, 31	latleeqm2 18476	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑉 ∈ (Base‘𝐾) ∧ ((𝑅‘𝐹) ∨ 𝑈) ∈ (Base‘𝐾)) → (𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈) ↔ (((𝑅‘𝐹) ∨ 𝑈) ∧ 𝑉) = 𝑉))
44	18, 21, 30, 43	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈) ↔ (((𝑅‘𝐹) ∨ 𝑈) ∧ 𝑉) = 𝑉))
45	42, 44	mpbid 232	. . . 4 ⊢ (𝜑 → (((𝑅‘𝐹) ∨ 𝑈) ∧ 𝑉) = 𝑉)
46		dia2dimlem3.d	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑇)
47		dia2dimlem3.q	. . . . . . 7 ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))
48		dia2dimlem3.uv	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
49	6, 15, 31, 7, 8, 9, 24, 47, 1, 27, 13, 5, 3, 35, 48, 39	dia2dimlem1 41029	. . . . . 6 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
50	6, 15, 31, 7, 8, 9, 24	trlval2 40128	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝑇 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑅‘𝐷) = ((𝑄 ∨ (𝐷‘𝑄)) ∧ 𝑊))
51	1, 46, 49, 50	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (𝑅‘𝐷) = ((𝑄 ∨ (𝐷‘𝑄)) ∧ 𝑊))
52	47	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
53		dia2dimlem3.dv	. . . . . . . . 9 ⊢ (𝜑 → (𝐷‘𝑄) = (𝐹‘𝑃))
54	52, 53	oveq12d 7421	. . . . . . . 8 ⊢ (𝜑 → (𝑄 ∨ (𝐷‘𝑄)) = (((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∨ (𝐹‘𝑃)))
55	5	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
56	19, 15, 7	hlatjcl 39331	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
57	2, 55, 28, 56	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
58	6, 15, 7	hlatlej1 39339	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ 𝑉))
59	2, 12, 14, 58	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ 𝑉))
60	19, 6, 15, 31, 7	atmod4i1 39831	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾)) ∧ (𝐹‘𝑃) ≤ ((𝐹‘𝑃) ∨ 𝑉)) → (((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∨ (𝐹‘𝑃)) = (((𝑃 ∨ 𝑈) ∨ (𝐹‘𝑃)) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
61	2, 12, 57, 23, 59, 60	syl131anc 1385	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∨ (𝐹‘𝑃)) = (((𝑃 ∨ 𝑈) ∨ (𝐹‘𝑃)) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
62	15, 7	hlatj32 39336	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴)) → ((𝑃 ∨ 𝑈) ∨ (𝐹‘𝑃)) = ((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈))
63	2, 55, 28, 12, 62	syl13anc 1374	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∨ (𝐹‘𝑃)) = ((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈))
64	63	oveq1d 7418	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ∨ 𝑈) ∨ (𝐹‘𝑃)) ∧ ((𝐹‘𝑃) ∨ 𝑉)) = (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
65	54, 61, 64	3eqtrd 2774	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∨ (𝐷‘𝑄)) = (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
66	65	oveq1d 7418	. . . . . 6 ⊢ (𝜑 → ((𝑄 ∨ (𝐷‘𝑄)) ∧ 𝑊) = ((((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊))
67		hlol 39325	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
68	2, 67	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ OL)
69	19, 15, 7	hlatjcl 39331	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
70	2, 55, 12, 69	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
71	19, 7	atbase 39253	. . . . . . . . 9 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
72	28, 71	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
73	19, 15	latjcl 18447	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∈ (Base‘𝐾))
74	18, 70, 72, 73	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∈ (Base‘𝐾))
75	1	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ 𝐻)
76	19, 8	lhpbase 39963	. . . . . . . 8 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
77	75, 76	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾))
78	19, 31	latm32 39195	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊) = ((((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ 𝑊) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
79	68, 74, 23, 77, 78	syl13anc 1374	. . . . . 6 ⊢ (𝜑 → ((((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊) = ((((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ 𝑊) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
80	6, 15, 31, 7, 8, 9, 24	trlval2 40128	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
81	1, 4, 5, 80	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
82	81	oveq1d 7418	. . . . . . . 8 ⊢ (𝜑 → ((𝑅‘𝐹) ∨ 𝑈) = (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∨ 𝑈))
83	27	simprd 495	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
84	19, 6, 15, 31, 7	atmod4i1 39831	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑈 ∈ 𝐴 ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑈 ≤ 𝑊) → (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∨ 𝑈) = (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ 𝑊))
85	2, 28, 70, 77, 83, 84	syl131anc 1385	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∨ 𝑈) = (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ 𝑊))
86	82, 85	eqtr2d 2771	. . . . . . 7 ⊢ (𝜑 → (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ 𝑊) = ((𝑅‘𝐹) ∨ 𝑈))
87	86	oveq1d 7418	. . . . . 6 ⊢ (𝜑 → ((((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑈) ∧ 𝑊) ∧ ((𝐹‘𝑃) ∨ 𝑉)) = (((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
88	66, 79, 87	3eqtrd 2774	. . . . 5 ⊢ (𝜑 → ((𝑄 ∨ (𝐷‘𝑄)) ∧ 𝑊) = (((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
89	51, 88	eqtr2d 2771	. . . 4 ⊢ (𝜑 → (((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) = (𝑅‘𝐷))
90	34, 45, 89	3brtr3d 5150	. . 3 ⊢ (𝜑 → 𝑉 ≤ (𝑅‘𝐷))
91		hlatl 39324	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
92	2, 91	syl 17	. . . 4 ⊢ (𝜑 → 𝐾 ∈ AtLat)
93		hlop 39326	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
94	2, 93	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ OP)
95		eqid 2735	. . . . . . . . . 10 ⊢ (0.‘𝐾) = (0.‘𝐾)
96		eqid 2735	. . . . . . . . . 10 ⊢ (lt‘𝐾) = (lt‘𝐾)
97	95, 96, 7	0ltat 39255	. . . . . . . . 9 ⊢ ((𝐾 ∈ OP ∧ 𝑉 ∈ 𝐴) → (0.‘𝐾)(lt‘𝐾)𝑉)
98	94, 14, 97	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (0.‘𝐾)(lt‘𝐾)𝑉)
99		hlpos 39330	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
100	2, 99	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Poset)
101	19, 95	op0cl 39148	. . . . . . . . . 10 ⊢ (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
102	94, 101	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0.‘𝐾) ∈ (Base‘𝐾))
103	19, 8, 9, 24	trlcl 40129	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) → (𝑅‘𝐷) ∈ (Base‘𝐾))
104	1, 46, 103	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐷) ∈ (Base‘𝐾))
105	19, 6, 96	pltletr 18351	. . . . . . . . 9 ⊢ ((𝐾 ∈ Poset ∧ ((0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ (𝑅‘𝐷) ∈ (Base‘𝐾))) → (((0.‘𝐾)(lt‘𝐾)𝑉 ∧ 𝑉 ≤ (𝑅‘𝐷)) → (0.‘𝐾)(lt‘𝐾)(𝑅‘𝐷)))
106	100, 102, 21, 104, 105	syl13anc 1374	. . . . . . . 8 ⊢ (𝜑 → (((0.‘𝐾)(lt‘𝐾)𝑉 ∧ 𝑉 ≤ (𝑅‘𝐷)) → (0.‘𝐾)(lt‘𝐾)(𝑅‘𝐷)))
107	98, 90, 106	mp2and 699	. . . . . . 7 ⊢ (𝜑 → (0.‘𝐾)(lt‘𝐾)(𝑅‘𝐷))
108	19, 96, 95	opltn0 39154	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ (𝑅‘𝐷) ∈ (Base‘𝐾)) → ((0.‘𝐾)(lt‘𝐾)(𝑅‘𝐷) ↔ (𝑅‘𝐷) ≠ (0.‘𝐾)))
109	94, 104, 108	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((0.‘𝐾)(lt‘𝐾)(𝑅‘𝐷) ↔ (𝑅‘𝐷) ≠ (0.‘𝐾)))
110	107, 109	mpbid 232	. . . . . 6 ⊢ (𝜑 → (𝑅‘𝐷) ≠ (0.‘𝐾))
111	110	neneqd 2937	. . . . 5 ⊢ (𝜑 → ¬ (𝑅‘𝐷) = (0.‘𝐾))
112	95, 7, 8, 9, 24	trlator0 40136	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) → ((𝑅‘𝐷) ∈ 𝐴 ∨ (𝑅‘𝐷) = (0.‘𝐾)))
113	1, 46, 112	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((𝑅‘𝐷) ∈ 𝐴 ∨ (𝑅‘𝐷) = (0.‘𝐾)))
114	113	orcomd 871	. . . . . 6 ⊢ (𝜑 → ((𝑅‘𝐷) = (0.‘𝐾) ∨ (𝑅‘𝐷) ∈ 𝐴))
115	114	ord 864	. . . . 5 ⊢ (𝜑 → (¬ (𝑅‘𝐷) = (0.‘𝐾) → (𝑅‘𝐷) ∈ 𝐴))
116	111, 115	mpd 15	. . . 4 ⊢ (𝜑 → (𝑅‘𝐷) ∈ 𝐴)
117	6, 7	atcmp 39275	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑉 ∈ 𝐴 ∧ (𝑅‘𝐷) ∈ 𝐴) → (𝑉 ≤ (𝑅‘𝐷) ↔ 𝑉 = (𝑅‘𝐷)))
118	92, 14, 116, 117	syl3anc 1373	. . 3 ⊢ (𝜑 → (𝑉 ≤ (𝑅‘𝐷) ↔ 𝑉 = (𝑅‘𝐷)))
119	90, 118	mpbid 232	. 2 ⊢ (𝜑 → 𝑉 = (𝑅‘𝐷))
120	119	eqcomd 2741	1 ⊢ (𝜑 → (𝑅‘𝐷) = 𝑉)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2108   ≠ wne 2932   class class class wbr 5119  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  lecple 17276  Posetcpo 18317  ltcplt 18318  joincjn 18321  meetcmee 18322  0.cp0 18431  Latclat 18439  OPcops 39136  OLcol 39138  Atomscatm 39227  AtLatcal 39228  HLchlt 39314  LHypclh 39949  LTrncltrn 40066  trLctrl 40123

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-iin 4970  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-1st 7986  df-2nd 7987  df-map 8840  df-proset 18304  df-poset 18323  df-plt 18338  df-lub 18354  df-glb 18355  df-join 18356  df-meet 18357  df-p0 18433  df-p1 18434  df-lat 18440  df-clat 18507  df-oposet 39140  df-ol 39142  df-oml 39143  df-covers 39230  df-ats 39231  df-atl 39262  df-cvlat 39286  df-hlat 39315  df-llines 39463  df-psubsp 39468  df-pmap 39469  df-padd 39761  df-lhyp 39953  df-laut 39954  df-ldil 40069  df-ltrn 40070  df-trl 40124

This theorem is referenced by:  dia2dimlem5  41033