Theorem dia2dimlem1 41263

Description: Lemma for dia2dim 41276. Show properties of the auxiliary atom 𝑄. Part of proof of Lemma M in [Crawley] p. 121 line 3. (Contributed by NM, 8-Sep-2014.)

Hypotheses

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

Assertion

Ref	Expression
dia2dimlem1	⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))

Proof of Theorem dia2dimlem1

Step	Hyp	Ref	Expression
1		dia2dimlem1.q	. . 3 ⊢ 𝑄 = ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉))
2		dia2dimlem1.k	. . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
3	2	simpld 494	. . . 4 ⊢ (𝜑 → 𝐾 ∈ HL)
4		dia2dimlem1.p	. . . . 5 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
5	4	simpld 494	. . . 4 ⊢ (𝜑 → 𝑃 ∈ 𝐴)
6		dia2dimlem1.f	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃))
7		dia2dimlem1.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
8		dia2dimlem1.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
9		dia2dimlem1.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
10		dia2dimlem1.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
11		dia2dimlem1.r	. . . . . 6 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
12	7, 8, 9, 10, 11	trlat 40368	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝐹 ∈ 𝑇 ∧ (𝐹‘𝑃) ≠ 𝑃)) → (𝑅‘𝐹) ∈ 𝐴)
13	2, 4, 6, 12	syl3anc 1373	. . . 4 ⊢ (𝜑 → (𝑅‘𝐹) ∈ 𝐴)
14		dia2dimlem1.u	. . . . 5 ⊢ (𝜑 → (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊))
15	14	simpld 494	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
16	6	simpld 494	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝑇)
17	7, 8, 9, 10	ltrnel 40338	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
18	2, 16, 4, 17	syl3anc 1373	. . . . 5 ⊢ (𝜑 → ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊))
19	18	simpld 494	. . . 4 ⊢ (𝜑 → (𝐹‘𝑃) ∈ 𝐴)
20		dia2dimlem1.v	. . . . 5 ⊢ (𝜑 → (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊))
21	20	simpld 494	. . . 4 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
22	4	simprd 495	. . . . . 6 ⊢ (𝜑 → ¬ 𝑃 ≤ 𝑊)
23	7, 9, 10, 11	trlle 40383	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝑅‘𝐹) ≤ 𝑊)
24	2, 16, 23	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → (𝑅‘𝐹) ≤ 𝑊)
25	14	simprd 495	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ≤ 𝑊)
26	3	hllatd 39563	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Lat)
27		eqid 2734	. . . . . . . . . . 11 ⊢ (Base‘𝐾) = (Base‘𝐾)
28	27, 8	atbase 39488	. . . . . . . . . 10 ⊢ ((𝑅‘𝐹) ∈ 𝐴 → (𝑅‘𝐹) ∈ (Base‘𝐾))
29	13, 28	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑅‘𝐹) ∈ (Base‘𝐾))
30	27, 8	atbase 39488	. . . . . . . . . 10 ⊢ (𝑈 ∈ 𝐴 → 𝑈 ∈ (Base‘𝐾))
31	15, 30	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾))
32	2	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 ∈ 𝐻)
33	27, 9	lhpbase 40197	. . . . . . . . . 10 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
34	32, 33	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾))
35		dia2dimlem1.j	. . . . . . . . . 10 ⊢ ∨ = (join‘𝐾)
36	27, 7, 35	latjle12 18371	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ ((𝑅‘𝐹) ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → (((𝑅‘𝐹) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ ((𝑅‘𝐹) ∨ 𝑈) ≤ 𝑊))
37	26, 29, 31, 34, 36	syl13anc 1374	. . . . . . . 8 ⊢ (𝜑 → (((𝑅‘𝐹) ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ ((𝑅‘𝐹) ∨ 𝑈) ≤ 𝑊))
38	24, 25, 37	mpbi2and 712	. . . . . . 7 ⊢ (𝜑 → ((𝑅‘𝐹) ∨ 𝑈) ≤ 𝑊)
39	27, 8	atbase 39488	. . . . . . . . 9 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
40	5, 39	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ (Base‘𝐾))
41	27, 35, 8	hlatjcl 39566	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑅‘𝐹) ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → ((𝑅‘𝐹) ∨ 𝑈) ∈ (Base‘𝐾))
42	3, 13, 15, 41	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((𝑅‘𝐹) ∨ 𝑈) ∈ (Base‘𝐾))
43	27, 7	lattr 18365	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑅‘𝐹) ∨ 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 ≤ ((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝑅‘𝐹) ∨ 𝑈) ≤ 𝑊) → 𝑃 ≤ 𝑊))
44	26, 40, 42, 34, 43	syl13anc 1374	. . . . . . 7 ⊢ (𝜑 → ((𝑃 ≤ ((𝑅‘𝐹) ∨ 𝑈) ∧ ((𝑅‘𝐹) ∨ 𝑈) ≤ 𝑊) → 𝑃 ≤ 𝑊))
45	38, 44	mpan2d 694	. . . . . 6 ⊢ (𝜑 → (𝑃 ≤ ((𝑅‘𝐹) ∨ 𝑈) → 𝑃 ≤ 𝑊))
46	22, 45	mtod 198	. . . . 5 ⊢ (𝜑 → ¬ 𝑃 ≤ ((𝑅‘𝐹) ∨ 𝑈))
47	20	simprd 495	. . . . . . 7 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
48	18	simprd 495	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐹‘𝑃) ≤ 𝑊)
49		nbrne2 5116	. . . . . . 7 ⊢ ((𝑉 ≤ 𝑊 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊) → 𝑉 ≠ (𝐹‘𝑃))
50	47, 48, 49	syl2anc 584	. . . . . 6 ⊢ (𝜑 → 𝑉 ≠ (𝐹‘𝑃))
51	50	necomd 2985	. . . . 5 ⊢ (𝜑 → (𝐹‘𝑃) ≠ 𝑉)
52	46, 51	jca 511	. . . 4 ⊢ (𝜑 → (¬ 𝑃 ≤ ((𝑅‘𝐹) ∨ 𝑈) ∧ (𝐹‘𝑃) ≠ 𝑉))
53	26	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → 𝐾 ∈ Lat)
54	40	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → 𝑃 ∈ (Base‘𝐾))
55	27, 35, 8	hlatjcl 39566	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑉 ∨ 𝑈) ∈ (Base‘𝐾))
56	3, 21, 15, 55	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∨ 𝑈) ∈ (Base‘𝐾))
57	56	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → (𝑉 ∨ 𝑈) ∈ (Base‘𝐾))
58	34	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → 𝑊 ∈ (Base‘𝐾))
59	7, 35, 8	hlatlej2 39575	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → 𝑉 ≤ ((𝐹‘𝑃) ∨ 𝑉))
60	3, 19, 21, 59	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ≤ ((𝐹‘𝑃) ∨ 𝑉))
61	60	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → 𝑉 ≤ ((𝐹‘𝑃) ∨ 𝑉))
62		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉))
63	61, 62	breqtrrd 5124	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → 𝑉 ≤ (𝑃 ∨ 𝑈))
64		dia2dimlem1.uv	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
65	64	necomd 2985	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ≠ 𝑈)
66	7, 35, 8	hlatexch2 39595	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑉 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ 𝑉 ≠ 𝑈) → (𝑉 ≤ (𝑃 ∨ 𝑈) → 𝑃 ≤ (𝑉 ∨ 𝑈)))
67	3, 21, 5, 15, 65, 66	syl131anc 1385	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 ≤ (𝑃 ∨ 𝑈) → 𝑃 ≤ (𝑉 ∨ 𝑈)))
68	67	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → (𝑉 ≤ (𝑃 ∨ 𝑈) → 𝑃 ≤ (𝑉 ∨ 𝑈)))
69	63, 68	mpd 15	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → 𝑃 ≤ (𝑉 ∨ 𝑈))
70	27, 8	atbase 39488	. . . . . . . . . . . 12 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
71	21, 70	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
72	27, 7, 35	latjle12 18371	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑉 ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ (𝑉 ∨ 𝑈) ≤ 𝑊))
73	26, 71, 31, 34, 72	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ≤ 𝑊 ∧ 𝑈 ≤ 𝑊) ↔ (𝑉 ∨ 𝑈) ≤ 𝑊))
74	47, 25, 73	mpbi2and 712	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 ∨ 𝑈) ≤ 𝑊)
75	74	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → (𝑉 ∨ 𝑈) ≤ 𝑊)
76	27, 7, 53, 54, 57, 58, 69, 75	lattrd 18367	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉)) → 𝑃 ≤ 𝑊)
77	76	ex 412	. . . . . 6 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) = ((𝐹‘𝑃) ∨ 𝑉) → 𝑃 ≤ 𝑊))
78	77	necon3bd 2944	. . . . 5 ⊢ (𝜑 → (¬ 𝑃 ≤ 𝑊 → (𝑃 ∨ 𝑈) ≠ ((𝐹‘𝑃) ∨ 𝑉)))
79	22, 78	mpd 15	. . . 4 ⊢ (𝜑 → (𝑃 ∨ 𝑈) ≠ ((𝐹‘𝑃) ∨ 𝑉))
80	7, 35, 8	hlatlej2 39575	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → (𝐹‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃)))
81	3, 5, 19, 80	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝐹‘𝑃) ≤ (𝑃 ∨ (𝐹‘𝑃)))
82		dia2dimlem1.m	. . . . . . . . . 10 ⊢ ∧ = (meet‘𝐾)
83	7, 35, 82, 8, 9, 10, 11	trlval2 40362	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
84	2, 16, 4, 83	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝑅‘𝐹) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊))
85	84	oveq2d 7372	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∨ (𝑅‘𝐹)) = (𝑃 ∨ ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)))
86	27, 35, 8	hlatjcl 39566	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
87	3, 5, 19, 86	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾))
88	7, 35, 8	hlatlej1 39574	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ (𝐹‘𝑃)))
89	3, 5, 19, 88	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → 𝑃 ≤ (𝑃 ∨ (𝐹‘𝑃)))
90	27, 7, 35, 82, 8	atmod3i1 40063	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑃 ≤ (𝑃 ∨ (𝐹‘𝑃))) → (𝑃 ∨ ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑃 ∨ 𝑊)))
91	3, 5, 87, 34, 89, 90	syl131anc 1385	. . . . . . . 8 ⊢ (𝜑 → (𝑃 ∨ ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑃 ∨ 𝑊)))
92		eqid 2734	. . . . . . . . . . . 12 ⊢ (1.‘𝐾) = (1.‘𝐾)
93	7, 35, 92, 8, 9	lhpjat2 40220	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ 𝑊) = (1.‘𝐾))
94	2, 4, 93	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑃 ∨ 𝑊) = (1.‘𝐾))
95	94	oveq2d 7372	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑃 ∨ 𝑊)) = ((𝑃 ∨ (𝐹‘𝑃)) ∧ (1.‘𝐾)))
96		hlol 39560	. . . . . . . . . . 11 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
97	3, 96	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ OL)
98	27, 82, 92	olm11 39426	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OL ∧ (𝑃 ∨ (𝐹‘𝑃)) ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (1.‘𝐾)) = (𝑃 ∨ (𝐹‘𝑃)))
99	97, 87, 98	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (1.‘𝐾)) = (𝑃 ∨ (𝐹‘𝑃)))
100	95, 99	eqtrd 2769	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∨ (𝐹‘𝑃)) ∧ (𝑃 ∨ 𝑊)) = (𝑃 ∨ (𝐹‘𝑃)))
101	91, 100	eqtrd 2769	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∨ ((𝑃 ∨ (𝐹‘𝑃)) ∧ 𝑊)) = (𝑃 ∨ (𝐹‘𝑃)))
102	85, 101	eqtrd 2769	. . . . . 6 ⊢ (𝜑 → (𝑃 ∨ (𝑅‘𝐹)) = (𝑃 ∨ (𝐹‘𝑃)))
103	81, 102	breqtrrd 5124	. . . . 5 ⊢ (𝜑 → (𝐹‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹)))
104		dia2dimlem1.rf	. . . . . . 7 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑈 ∨ 𝑉))
105	35, 8	hlatjcom 39567	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (𝑈 ∨ 𝑉) = (𝑉 ∨ 𝑈))
106	3, 15, 21, 105	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∨ 𝑉) = (𝑉 ∨ 𝑈))
107	104, 106	breqtrd 5122	. . . . . 6 ⊢ (𝜑 → (𝑅‘𝐹) ≤ (𝑉 ∨ 𝑈))
108		dia2dimlem1.ru	. . . . . . 7 ⊢ (𝜑 → (𝑅‘𝐹) ≠ 𝑈)
109	7, 35, 8	hlatexch2 39595	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ ((𝑅‘𝐹) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑅‘𝐹) ≠ 𝑈) → ((𝑅‘𝐹) ≤ (𝑉 ∨ 𝑈) → 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈)))
110	3, 13, 21, 15, 108, 109	syl131anc 1385	. . . . . 6 ⊢ (𝜑 → ((𝑅‘𝐹) ≤ (𝑉 ∨ 𝑈) → 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈)))
111	107, 110	mpd 15	. . . . 5 ⊢ (𝜑 → 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈))
112	103, 111	jca 511	. . . 4 ⊢ (𝜑 → ((𝐹‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹)) ∧ 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈)))
113	7, 35, 82, 8	ps-2c 39727	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (𝑅‘𝐹) ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) ∧ ((¬ 𝑃 ≤ ((𝑅‘𝐹) ∨ 𝑈) ∧ (𝐹‘𝑃) ≠ 𝑉) ∧ (𝑃 ∨ 𝑈) ≠ ((𝐹‘𝑃) ∨ 𝑉) ∧ ((𝐹‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹)) ∧ 𝑉 ≤ ((𝑅‘𝐹) ∨ 𝑈)))) → ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∈ 𝐴)
114	3, 5, 13, 15, 19, 21, 52, 79, 112, 113	syl333anc 1404	. . 3 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ∈ 𝐴)
115	1, 114	eqeltrid 2838	. 2 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
116	27, 35, 8	hlatjcl 39566	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
117	3, 5, 15, 116	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑃 ∨ 𝑈) ∈ (Base‘𝐾))
118	27, 35, 8	hlatjcl 39566	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝐹‘𝑃) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾))
119	3, 19, 21, 118	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾))
120	27, 7, 82	latmle1 18385	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ≤ (𝑃 ∨ 𝑈))
121	26, 117, 119, 120	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ≤ (𝑃 ∨ 𝑈))
122	1, 121	eqbrtrid 5131	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ≤ (𝑃 ∨ 𝑈))
123	27, 8	atbase 39488	. . . . . . . . . . . . 13 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
124	115, 123	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝐾))
125	27, 7, 82	latlem12 18387	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 ≤ (𝑃 ∨ 𝑈) ∧ 𝑄 ≤ 𝑊) ↔ 𝑄 ≤ ((𝑃 ∨ 𝑈) ∧ 𝑊)))
126	26, 124, 117, 34, 125	syl13anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄 ≤ (𝑃 ∨ 𝑈) ∧ 𝑄 ≤ 𝑊) ↔ 𝑄 ≤ ((𝑃 ∨ 𝑈) ∧ 𝑊)))
127	126	biimpd 229	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 ≤ (𝑃 ∨ 𝑈) ∧ 𝑄 ≤ 𝑊) → 𝑄 ≤ ((𝑃 ∨ 𝑈) ∧ 𝑊)))
128	122, 127	mpand 695	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 ≤ 𝑊 → 𝑄 ≤ ((𝑃 ∨ 𝑈) ∧ 𝑊)))
129	128	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑄 ≤ ((𝑃 ∨ 𝑈) ∧ 𝑊))
130		eqid 2734	. . . . . . . . . . . . 13 ⊢ (0.‘𝐾) = (0.‘𝐾)
131	7, 82, 130, 8, 9	lhpmat 40229	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∧ 𝑊) = (0.‘𝐾))
132	2, 4, 131	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑃 ∧ 𝑊) = (0.‘𝐾))
133	132	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃 ∧ 𝑊) ∨ 𝑈) = ((0.‘𝐾) ∨ 𝑈))
134	27, 7, 35, 82, 8	atmod4i1 40065	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑈 ∈ 𝐴 ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑈 ≤ 𝑊) → ((𝑃 ∧ 𝑊) ∨ 𝑈) = ((𝑃 ∨ 𝑈) ∧ 𝑊))
135	3, 15, 40, 34, 25, 134	syl131anc 1385	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑃 ∧ 𝑊) ∨ 𝑈) = ((𝑃 ∨ 𝑈) ∧ 𝑊))
136	27, 35, 130	olj02 39425	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OL ∧ 𝑈 ∈ (Base‘𝐾)) → ((0.‘𝐾) ∨ 𝑈) = 𝑈)
137	97, 31, 136	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((0.‘𝐾) ∨ 𝑈) = 𝑈)
138	133, 135, 137	3eqtr3d 2777	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∧ 𝑊) = 𝑈)
139	138	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → ((𝑃 ∨ 𝑈) ∧ 𝑊) = 𝑈)
140	129, 139	breqtrd 5122	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑄 ≤ 𝑈)
141		hlatl 39559	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
142	3, 141	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ AtLat)
143	142	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝐾 ∈ AtLat)
144	115	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑄 ∈ 𝐴)
145	15	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑈 ∈ 𝐴)
146	7, 8	atcmp 39510	. . . . . . . 8 ⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑄 ≤ 𝑈 ↔ 𝑄 = 𝑈))
147	143, 144, 145, 146	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → (𝑄 ≤ 𝑈 ↔ 𝑄 = 𝑈))
148	140, 147	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑄 = 𝑈)
149	27, 7, 82	latmle2 18386	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑈) ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ≤ ((𝐹‘𝑃) ∨ 𝑉))
150	26, 117, 119, 149	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 ∨ 𝑈) ∧ ((𝐹‘𝑃) ∨ 𝑉)) ≤ ((𝐹‘𝑃) ∨ 𝑉))
151	1, 150	eqbrtrid 5131	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ≤ ((𝐹‘𝑃) ∨ 𝑉))
152	27, 7, 82	latlem12 18387	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝐹‘𝑃) ∨ 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 ≤ ((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑄 ≤ 𝑊) ↔ 𝑄 ≤ (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊)))
153	26, 124, 119, 34, 152	syl13anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑄 ≤ ((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑄 ≤ 𝑊) ↔ 𝑄 ≤ (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊)))
154	153	biimpd 229	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑄 ≤ ((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑄 ≤ 𝑊) → 𝑄 ≤ (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊)))
155	151, 154	mpand 695	. . . . . . . . 9 ⊢ (𝜑 → (𝑄 ≤ 𝑊 → 𝑄 ≤ (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊)))
156	155	imp 406	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑄 ≤ (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊))
157	7, 82, 130, 8, 9	lhpmat 40229	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹‘𝑃) ∈ 𝐴 ∧ ¬ (𝐹‘𝑃) ≤ 𝑊)) → ((𝐹‘𝑃) ∧ 𝑊) = (0.‘𝐾))
158	2, 18, 157	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹‘𝑃) ∧ 𝑊) = (0.‘𝐾))
159	158	oveq1d 7371	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐹‘𝑃) ∧ 𝑊) ∨ 𝑉) = ((0.‘𝐾) ∨ 𝑉))
160	27, 8	atbase 39488	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑃) ∈ 𝐴 → (𝐹‘𝑃) ∈ (Base‘𝐾))
161	19, 160	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐹‘𝑃) ∈ (Base‘𝐾))
162	27, 7, 35, 82, 8	atmod4i1 40065	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑉 ∈ 𝐴 ∧ (𝐹‘𝑃) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑉 ≤ 𝑊) → (((𝐹‘𝑃) ∧ 𝑊) ∨ 𝑉) = (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊))
163	3, 21, 161, 34, 47, 162	syl131anc 1385	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐹‘𝑃) ∧ 𝑊) ∨ 𝑉) = (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊))
164	27, 35, 130	olj02 39425	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OL ∧ 𝑉 ∈ (Base‘𝐾)) → ((0.‘𝐾) ∨ 𝑉) = 𝑉)
165	97, 71, 164	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((0.‘𝐾) ∨ 𝑉) = 𝑉)
166	159, 163, 165	3eqtr3d 2777	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊) = 𝑉)
167	166	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → (((𝐹‘𝑃) ∨ 𝑉) ∧ 𝑊) = 𝑉)
168	156, 167	breqtrd 5122	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑄 ≤ 𝑉)
169	21	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑉 ∈ 𝐴)
170	7, 8	atcmp 39510	. . . . . . . 8 ⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) → (𝑄 ≤ 𝑉 ↔ 𝑄 = 𝑉))
171	143, 144, 169, 170	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → (𝑄 ≤ 𝑉 ↔ 𝑄 = 𝑉))
172	168, 171	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑄 = 𝑉)
173	148, 172	eqtr3d 2771	. . . . 5 ⊢ ((𝜑 ∧ 𝑄 ≤ 𝑊) → 𝑈 = 𝑉)
174	173	ex 412	. . . 4 ⊢ (𝜑 → (𝑄 ≤ 𝑊 → 𝑈 = 𝑉))
175	174	necon3ad 2943	. . 3 ⊢ (𝜑 → (𝑈 ≠ 𝑉 → ¬ 𝑄 ≤ 𝑊))
176	64, 175	mpd 15	. 2 ⊢ (𝜑 → ¬ 𝑄 ≤ 𝑊)
177	115, 176	jca 511	1 ⊢ (𝜑 → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2930   class class class wbr 5096  ‘cfv 6490  (class class class)co 7356  Basecbs 17134  lecple 17182  joincjn 18232  meetcmee 18233  0.cp0 18342  1.cp1 18343  Latclat 18352  OLcol 39373  Atomscatm 39462  AtLatcal 39463  HLchlt 39549  LHypclh 40183  LTrncltrn 40300  trLctrl 40357

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-iin 4947  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-map 8763  df-proset 18215  df-poset 18234  df-plt 18249  df-lub 18265  df-glb 18266  df-join 18267  df-meet 18268  df-p0 18344  df-p1 18345  df-lat 18353  df-clat 18420  df-oposet 39375  df-ol 39377  df-oml 39378  df-covers 39465  df-ats 39466  df-atl 39497  df-cvlat 39521  df-hlat 39550  df-llines 39697  df-psubsp 39702  df-pmap 39703  df-padd 39995  df-lhyp 40187  df-laut 40188  df-ldil 40303  df-ltrn 40304  df-trl 40358

This theorem is referenced by:  dia2dimlem3  41265  dia2dimlem6  41268