cdlemi - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemi		Structured version Visualization version GIF version

Theorem cdlemi 41970

Description: Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)

**Hypotheses**
Ref	Expression
cdlemi.b	⊢ 𝐵 = (Base‘𝐾)
cdlemi.l	⊢ ≤ = (le‘𝐾)
cdlemi.j	⊢ ∨ = (join‘𝐾)
cdlemi.m	⊢ ∧ = (meet‘𝐾)
cdlemi.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemi.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemi.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemi.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemi.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
cdlemi.s	⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))

**Assertion**
Ref	Expression
cdlemi	⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) = 𝑆)

**Proof of Theorem cdlemi**
Step	Hyp	Ref	Expression
1		simp11l 1303	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ HL)
2		simp11r 1304	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑊 ∈ 𝐻)
3		simp2l 1218	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑈 ∈ 𝐸)
4		simp13 1224	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇)
5		simp2r 1219	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
6		cdlemi.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
7		cdlemi.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
8		cdlemi.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
9		cdlemi.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
10		cdlemi.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
11		cdlemi.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
12		cdlemi.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
13		cdlemi.r	. . . . . 6 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
14		cdlemi.e	. . . . . 6 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
15	6, 7, 8, 9, 10, 11, 12, 13, 14	cdlemi1 41968	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)))
16	1, 2, 3, 4, 5, 15	syl221anc 1408	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)))
17		simp12 1223	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇)
18	6, 7, 8, 9, 10, 11, 12, 13, 14	cdlemi2 41969	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
19	1, 2, 3, 17, 4, 5, 18	syl231anc 1417	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
20	1	hllatd 40514	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ Lat)
21		simp11 1222	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22	11, 12, 14	tendocl 41917	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑈‘𝐺) ∈ 𝑇)
23	21, 3, 4, 22	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑈‘𝐺) ∈ 𝑇)
24		simp2rl 1261	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐴)
25	6, 10	atbase 40439	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
26	24, 25	syl 18	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐵)
27	6, 11, 12	ltrncl 41275	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐺) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐵)
28	21, 23, 26, 27	syl3anc 1398	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐵)
29	6, 11, 12, 13	trlcl 41314	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ 𝐵)
30	21, 4, 29	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ 𝐵)
31	6, 8	latjcl 18618	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ (𝑅‘𝐺) ∈ 𝐵) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
32	20, 26, 30, 31	syl3anc 1398	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
33	11, 12, 14	tendocl 41917	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑈‘𝐹) ∈ 𝑇)
34	21, 3, 17, 33	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑈‘𝐹) ∈ 𝑇)
35	6, 11, 12	ltrncl 41275	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐹) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → ((𝑈‘𝐹)‘𝑃) ∈ 𝐵)
36	21, 34, 26, 35	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐹)‘𝑃) ∈ 𝐵)
37	11, 12	ltrncnv 41296	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
38	21, 17, 37	syl2anc 596	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ∈ 𝑇)
39	11, 12	ltrnco 41869	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
40	21, 4, 38, 39	syl3anc 1398	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
41	6, 11, 12, 13	trlcl 41314	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
42	21, 40, 41	syl2anc 596	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
43	6, 8	latjcl 18618	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑈‘𝐹)‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵) → (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
44	20, 36, 42, 43	syl3anc 1398	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
45	6, 7, 9	latlem12 18645	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (((𝑈‘𝐺)‘𝑃) ∈ 𝐵 ∧ (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵 ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)) → ((((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
46	20, 28, 32, 44, 45	syl13anc 1399	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
47	16, 19, 46	mpbi2and 725	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
48		hlatl 40510	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
49	1, 48	syl 18	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ AtLat)
50	7, 10, 11, 12	ltrnat 41290	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐺) ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐴)
51	21, 23, 24, 50	syl3anc 1398	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐴)
52	7, 10, 11, 12	ltrnel 41289	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐹) ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊))
53	21, 34, 5, 52	syl3anc 1398	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊))
54	6, 7, 8, 9, 10, 11, 12, 13, 14	cdlemi1 41968	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹)))
55	1, 2, 3, 17, 5, 54	syl221anc 1408	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹)))
56	5, 53, 55	3jca 1146	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊) ∧ ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹))))
57		eqid 2760	. . . . . . 7 ⊢ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
58	6, 7, 8, 9, 10, 11, 12, 13, 57	cdlemh 41967	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊) ∧ ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∧ ¬ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ≤ 𝑊))
59	58	simpld 500	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊) ∧ ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴)
60	56, 59	syld3an2 1438	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴)
61	7, 10	atcmp 40461	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ ((𝑈‘𝐺)‘𝑃) ∈ 𝐴 ∧ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴) → (((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
62	49, 51, 60, 61	syl3anc 1398	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
63	47, 62	mpbid 235	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
64		cdlemi.s	. 2 ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
65	63, 64	eqtr4di 2813	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) = 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 I cid 5544 ^◡ccnv 5649 ↾ cres 5652 ∘ ccom 5654 ‘cfv 6538 (class class class)co 7420 Basecbs 17392 lecple 17440 joincjn 18490 meetcmee 18491 Latclat 18610 Atomscatm 40413 AtLatcal 40414 HLchlt 40500 LHypclh 41134 LTrncltrn 41251 trLctrl 41308 TEndoctendo 41902

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-riotaBAD 40103

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-undef 8293 df-map 8852 df-proset 18473 df-poset 18492 df-plt 18507 df-lub 18523 df-glb 18524 df-join 18525 df-meet 18526 df-p0 18602 df-p1 18603 df-lat 18611 df-clat 18678 df-oposet 40326 df-ol 40328 df-oml 40329 df-covers 40416 df-ats 40417 df-atl 40448 df-cvlat 40472 df-hlat 40501 df-llines 40648 df-lplanes 40649 df-lvols 40650 df-lines 40651 df-psubsp 40653 df-pmap 40654 df-padd 40946 df-lhyp 41138 df-laut 41139 df-ldil 41254 df-ltrn 41255 df-trl 41309 df-tendo 41905

This theorem is used by: cdlemj1 41971

W3C validator