Theorem dia2dimlem2 41728

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

Hypotheses

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

Assertion

Ref	Expression
dia2dimlem2	⊢ (𝜑 → (𝑅‘𝐺) = 𝑈)

Proof of Theorem dia2dimlem2

Step	Hyp	Ref	Expression
1		dia2dimlem2.k	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2	1	simpld 499	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ HL)
3	2	hllatd 40027	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Lat)
4		dia2dimlem2.p	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
5	4	simpld 499	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
6		eqid 2769	. . . . . . . . 9 ⊢ (Base‘𝐾) = (Base‘𝐾)
7		dia2dimlem2.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
8	6, 7	atbase 39952	. . . . . . . 8 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
9	5, 8	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝐾))
10		dia2dimlem2.u	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
11	10	simpld 499	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
12	6, 7	atbase 39952	. . . . . . . 8 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
13	11, 12	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
14		dia2dimlem2.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
15		dia2dimlem2.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
16	6, 14, 15	latlej2 18504	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → 𝑈 ≤ (𝑃 ∨ 𝑈))
17	3, 9, 13, 16	syl3anc 1396	. . . . . 6 ⊢ (𝜑 → 𝑈 ≤ (𝑃 ∨ 𝑈))
18	6, 15, 7	hlatjcl 40030	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
19	2, 5, 11, 18	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
20		dia2dimlem2.m	. . . . . . . 8 ⊢ ∧ = (meet‘𝐾)
21	6, 14, 20	latleeqm2 18523	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾)) → (𝑈 ≤ (𝑃 ∨ 𝑈) ↔ ((𝑃 ∨ 𝑈) ∧ 𝑈) = 𝑈))
22	3, 13, 19, 21	syl3anc 1396	. . . . . 6 ⊢ (𝜑 → (𝑈 ≤ (𝑃 ∨ 𝑈) ↔ ((𝑃 ∨ 𝑈) ∧ 𝑈) = 𝑈))
23	17, 22	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∧ 𝑈) = 𝑈)
24		dia2dimlem2.rf	. . . . . . . 8 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
25		dia2dimlem2.f	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
26		dia2dimlem2.h	. . . . . . . . . . 11 ⊢ 𝐻 = (LHyp‘𝐾)
27		dia2dimlem2.t	. . . . . . . . . . 11 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
28		dia2dimlem2.r	. . . . . . . . . . 11 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
29	14, 7, 26, 27, 28	trlat 40832	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ∈ 𝐴)
30	1, 4, 25, 29	syl3anc 1396	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐹) ∈ 𝐴)
31		dia2dimlem2.v	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
32	31	simpld 499	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
33		dia2dimlem2.rv	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑉)
34	14, 15, 7	hlatexch2 40059	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝐹) ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) ∧ (𝑅‘𝐹) ≠ 𝑉) → ((𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉) → 𝑈 ≤ ((𝑅‘𝐹) ∨ 𝑉)))
35	2, 30, 11, 32, 33, 34	syl131anc 1408	. . . . . . . 8 ⊢ (𝜑 → ((𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉) → 𝑈 ≤ ((𝑅‘𝐹) ∨ 𝑉)))
36	24, 35	mpd 16	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≤ ((𝑅‘𝐹) ∨ 𝑉))
37	25	simpld 499	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
38	14, 15, 20, 7, 26, 27, 28	trlval2 40826	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
39	1, 37, 4, 38	syl3anc 1396	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
40	39	oveq1d 7426	. . . . . . . 8 ⊢ (𝜑 → ((𝑅‘𝐹) ∨ 𝑉) = (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∨ 𝑉))
41	14, 7, 26, 27	ltrnel 40802	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
42	1, 37, 4, 41	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
43	42	simpld 499	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝑃) ∈ 𝐴)
44	6, 15, 7	hlatjcl 40030	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
45	2, 5, 43, 44	syl3anc 1396	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
46	1	simprd 500	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ 𝐻)
47	6, 26	lhpbase 40661	. . . . . . . . . . 11 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
48	46, 47	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾))
49	31	simprd 500	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
50	6, 14, 15, 20, 7	atmod4i1 40529	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑉 ∈ 𝐴 ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 ≤ 𝑊) → (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∨ 𝑉) = (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑉) ∧ 𝑊))
51	2, 32, 45, 48, 49, 50	syl131anc 1408	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∨ 𝑉) = (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑉) ∧ 𝑊))
52	15, 7	hlatjass 40033	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴)) → ((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑉) = (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)))
53	2, 5, 43, 32, 52	syl13anc 1397	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑉) = (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)))
54	53	oveq1d 7426	. . . . . . . . 9 ⊢ (𝜑 → (((𝑃 ∨ (𝐹‘𝑃)) ∨ 𝑉) ∧ 𝑊) = ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊))
55	51, 54	eqtrd 2804	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊) ∨ 𝑉) = ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊))
56	40, 55	eqtrd 2804	. . . . . . 7 ⊢ (𝜑 → ((𝑅‘𝐹) ∨ 𝑉) = ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊))
57	36, 56	breqtrd 5141	. . . . . 6 ⊢ (𝜑 → 𝑈 ≤ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊))
58	6, 15, 7	hlatjcl 40030	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾))
59	2, 43, 32, 58	syl3anc 1396	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾))
60	6, 15	latjcl 18494	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾)) → (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∈ (Base‘𝐾))
61	3, 9, 59, 60	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∈ (Base‘𝐾))
62	6, 20	latmcl 18495	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊) ∈ (Base‘𝐾))
63	3, 61, 48, 62	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊) ∈ (Base‘𝐾))
64	6, 14, 20	latmlem2 18525	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑈 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))) → (𝑈 ≤ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊) → ((𝑃 ∨ 𝑈) ∧ 𝑈) ≤ ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊))))
65	3, 13, 63, 19, 64	syl13anc 1397	. . . . . 6 ⊢ (𝜑 → (𝑈 ≤ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊) → ((𝑃 ∨ 𝑈) ∧ 𝑈) ≤ ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊))))
66	57, 65	mpd 16	. . . . 5 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∧ 𝑈) ≤ ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)))
67	23, 66	eqbrtrrd 5139	. . . 4 ⊢ (𝜑 → 𝑈 ≤ ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)))
68		dia2dimlem2.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ 𝑇)
69	14, 15, 20, 7, 26, 27, 28	trlval2 40826	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊))
70	1, 68, 4, 69	syl3anc 1396	. . . . . 6 ⊢ (𝜑 → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊))
71		dia2dimlem2.gv	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺‘𝑃) = 𝑄)
72		dia2dimlem2.q	. . . . . . . . . 10 ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))
73	71, 72	eqtrdi 2820	. . . . . . . . 9 ⊢ (𝜑 → (𝐺‘𝑃) = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)))
74	73	oveq2d 7427	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∨ (𝐺‘𝑃)) = (𝑃 ∨ ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))))
75	74	oveq1d 7426	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) = ((𝑃 ∨ ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))) ∧ 𝑊))
76	14, 15, 7	hlatlej1 40038	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑈))
77	2, 5, 11, 76	syl3anc 1396	. . . . . . . . . 10 ⊢ (𝜑 → 𝑃 ≤ (𝑃 ∨ 𝑈))
78	6, 14, 15, 20, 7	atmod3i1 40527	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ 𝑈)) → (𝑃 ∨ ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))) = ((𝑃 ∨ 𝑈) ∧ (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉))))
79	2, 5, 19, 59, 77, 78	syl131anc 1408	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∨ ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))) = ((𝑃 ∨ 𝑈) ∧ (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉))))
80	79	oveq1d 7426	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∨ ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))) ∧ 𝑊) = (((𝑃 ∨ 𝑈) ∧ (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉))) ∧ 𝑊))
81		hlol 40024	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
82	2, 81	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ OL)
83	6, 20	latmassOLD 39892	. . . . . . . . 9 ⊢ ((𝐾 ∈ OL ∧ ((𝑃 ∨ 𝑈) ∈ (Base‘𝐾) ∧ (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑃 ∨ 𝑈) ∧ (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉))) ∧ 𝑊) = ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)))
84	82, 19, 61, 48, 83	syl13anc 1397	. . . . . . . 8 ⊢ (𝜑 → (((𝑃 ∨ 𝑈) ∧ (𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉))) ∧ 𝑊) = ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)))
85	80, 84	eqtrd 2804	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ∨ ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))) ∧ 𝑊) = ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)))
86	75, 85	eqtrd 2804	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) = ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)))
87	70, 86	eqtrd 2804	. . . . 5 ⊢ (𝜑 → (𝑅‘𝐺) = ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)))
88	87	eqcomd 2775	. . . 4 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∧ ((𝑃 ∨ ((𝐹‘𝑃) ∨ 𝑉)) ∧ 𝑊)) = (𝑅‘𝐺))
89	67, 88	breqtrd 5141	. . 3 ⊢ (𝜑 → 𝑈 ≤ (𝑅‘𝐺))
90		hlatl 40023	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
91	2, 90	syl 18	. . . 4 ⊢ (𝜑 → 𝐾 ∈ AtLat)
92		hlop 40025	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
93	2, 92	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ OP)
94		eqid 2769	. . . . . . . . . 10 ⊢ (0.‘𝐾) = (0.‘𝐾)
95		eqid 2769	. . . . . . . . . 10 ⊢ (lt‘𝐾) = (lt‘𝐾)
96	94, 95, 7	0ltat 39954	. . . . . . . . 9 ⊢ ((𝐾 ∈ OP ∧ 𝑈 ∈ 𝐴) → (0.‘𝐾)(lt‘𝐾)𝑈)
97	93, 11, 96	syl2anc 595	. . . . . . . 8 ⊢ (𝜑 → (0.‘𝐾)(lt‘𝐾)𝑈)
98		hlpos 40029	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
99	2, 98	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Poset)
100	6, 94	op0cl 39847	. . . . . . . . . 10 ⊢ (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
101	93, 100	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (0.‘𝐾) ∈ (Base‘𝐾))
102	6, 26, 27, 28	trlcl 40827	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ (Base‘𝐾))
103	1, 68, 102	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐺) ∈ (Base‘𝐾))
104	6, 14, 95	pltletr 18396	. . . . . . . . 9 ⊢ ((𝐾 ∈ Poset ∧ ((0.‘𝐾) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ (𝑅‘𝐺) ∈ (Base‘𝐾))) → (((0.‘𝐾)(lt‘𝐾)𝑈 ∧ 𝑈 ≤ (𝑅‘𝐺)) → (0.‘𝐾)(lt‘𝐾)(𝑅‘𝐺)))
105	99, 101, 13, 103, 104	syl13anc 1397	. . . . . . . 8 ⊢ (𝜑 → (((0.‘𝐾)(lt‘𝐾)𝑈 ∧ 𝑈 ≤ (𝑅‘𝐺)) → (0.‘𝐾)(lt‘𝐾)(𝑅‘𝐺)))
106	97, 89, 105	mp2and 711	. . . . . . 7 ⊢ (𝜑 → (0.‘𝐾)(lt‘𝐾)(𝑅‘𝐺))
107	6, 95, 94	opltn0 39853	. . . . . . . 8 ⊢ ((𝐾 ∈ OP ∧ (𝑅‘𝐺) ∈ (Base‘𝐾)) → ((0.‘𝐾)(lt‘𝐾)(𝑅‘𝐺) ↔ (𝑅‘𝐺) ≠ (0.‘𝐾)))
108	93, 103, 107	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → ((0.‘𝐾)(lt‘𝐾)(𝑅‘𝐺) ↔ (𝑅‘𝐺) ≠ (0.‘𝐾)))
109	106, 108	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝑅‘𝐺) ≠ (0.‘𝐾))
110	109	neneqd 2969	. . . . 5 ⊢ (𝜑 → ¬ (𝑅‘𝐺) = (0.‘𝐾))
111	94, 7, 26, 27, 28	trlator0 40834	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → ((𝑅‘𝐺) ∈ 𝐴 ∨ (𝑅‘𝐺) = (0.‘𝐾)))
112	1, 68, 111	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → ((𝑅‘𝐺) ∈ 𝐴 ∨ (𝑅‘𝐺) = (0.‘𝐾)))
113	112	orcomd 884	. . . . . 6 ⊢ (𝜑 → ((𝑅‘𝐺) = (0.‘𝐾) ∨ (𝑅‘𝐺) ∈ 𝐴))
114	113	ord 877	. . . . 5 ⊢ (𝜑 → (¬ (𝑅‘𝐺) = (0.‘𝐾) → (𝑅‘𝐺) ∈ 𝐴))
115	110, 114	mpd 16	. . . 4 ⊢ (𝜑 → (𝑅‘𝐺) ∈ 𝐴)
116	14, 7	atcmp 39974	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑈 ∈ 𝐴 ∧ (𝑅‘𝐺) ∈ 𝐴) → (𝑈 ≤ (𝑅‘𝐺) ↔ 𝑈 = (𝑅‘𝐺)))
117	91, 11, 115, 116	syl3anc 1396	. . 3 ⊢ (𝜑 → (𝑈 ≤ (𝑅‘𝐺) ↔ 𝑈 = (𝑅‘𝐺)))
118	89, 117	mpbid 235	. 2 ⊢ (𝜑 → 𝑈 = (𝑅‘𝐺))
119	118	eqcomd 2775	1 ⊢ (𝜑 → (𝑅‘𝐺) = 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ≠ wne 2964   class class class wbr 5113  ‘cfv 6537  (class class class)co 7411  Basecbs 17268  lecple 17316  Posetcpo 18362  ltcplt 18363  joincjn 18366  meetcmee 18367  0.cp0 18476  Latclat 18486  OPcops 39835  OLcol 39837  Atomscatm 39926  AtLatcal 39927  HLchlt 40013  LHypclh 40647  LTrncltrn 40764  trLctrl 40821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986  df-map 8825  df-proset 18349  df-poset 18368  df-plt 18383  df-lub 18399  df-glb 18400  df-join 18401  df-meet 18402  df-p0 18478  df-p1 18479  df-lat 18487  df-clat 18554  df-oposet 39839  df-ol 39841  df-oml 39842  df-covers 39929  df-ats 39930  df-atl 39961  df-cvlat 39985  df-hlat 40014  df-psubsp 40166  df-pmap 40167  df-padd 40459  df-lhyp 40651  df-laut 40652  df-ldil 40767  df-ltrn 40768  df-trl 40822

This theorem is referenced by:  dia2dimlem5  41731