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 41076

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 1285	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ HL)
2		simp11r 1286	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑊 ∈ 𝐻)
3		simp2l 1200	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑈 ∈ 𝐸)
4		simp13 1206	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐺 ∈ 𝑇)
5		simp2r 1201	. . . . 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 41074	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)))
16	1, 2, 3, 4, 5, 15	syl221anc 1383	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)))
17		simp12 1205	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐹 ∈ 𝑇)
18	6, 7, 8, 9, 10, 11, 12, 13, 14	cdlemi2 41075	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
19	1, 2, 3, 17, 4, 5, 18	syl231anc 1392	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
20	1	hllatd 39620	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ Lat)
21		simp11 1204	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22	11, 12, 14	tendocl 41023	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇) → (𝑈‘𝐺) ∈ 𝑇)
23	21, 3, 4, 22	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑈‘𝐺) ∈ 𝑇)
24		simp2rl 1243	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐴)
25	6, 10	atbase 39545	. . . . . . 7 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
26	24, 25	syl 17	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝑃 ∈ 𝐵)
27	6, 11, 12	ltrncl 40381	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐺) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐵)
28	21, 23, 26, 27	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐵)
29	6, 11, 12, 13	trlcl 40420	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → (𝑅‘𝐺) ∈ 𝐵)
30	21, 4, 29	syl2anc 584	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘𝐺) ∈ 𝐵)
31	6, 8	latjcl 18362	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ (𝑅‘𝐺) ∈ 𝐵) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
32	20, 26, 30, 31	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵)
33	11, 12, 14	tendocl 41023	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑈‘𝐹) ∈ 𝑇)
34	21, 3, 17, 33	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑈‘𝐹) ∈ 𝑇)
35	6, 11, 12	ltrncl 40381	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐹) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵) → ((𝑈‘𝐹)‘𝑃) ∈ 𝐵)
36	21, 34, 26, 35	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐹)‘𝑃) ∈ 𝐵)
37	11, 12	ltrncnv 40402	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ^◡𝐹 ∈ 𝑇)
38	21, 17, 37	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ^◡𝐹 ∈ 𝑇)
39	11, 12	ltrnco 40975	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ^◡𝐹 ∈ 𝑇) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
40	21, 4, 38, 39	syl3anc 1373	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝐺 ∘ ^◡𝐹) ∈ 𝑇)
41	6, 11, 12, 13	trlcl 40420	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∘ ^◡𝐹) ∈ 𝑇) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
42	21, 40, 41	syl2anc 584	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵)
43	6, 8	latjcl 18362	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ ((𝑈‘𝐹)‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝐺 ∘ ^◡𝐹)) ∈ 𝐵) → (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
44	20, 36, 42, 43	syl3anc 1373	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)
45	6, 7, 9	latlem12 18389	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (((𝑈‘𝐺)‘𝑃) ∈ 𝐵 ∧ (𝑃 ∨ (𝑅‘𝐺)) ∈ 𝐵 ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))) ∈ 𝐵)) → ((((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
46	20, 28, 32, 44, 45	syl13anc 1374	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((((𝑈‘𝐺)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑈‘𝐺)‘𝑃) ≤ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
47	16, 19, 46	mpbi2and 712	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
48		hlatl 39616	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
49	1, 48	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → 𝐾 ∈ AtLat)
50	7, 10, 11, 12	ltrnat 40396	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐺) ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐴)
51	21, 23, 24, 50	syl3anc 1373	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) ∈ 𝐴)
52	7, 10, 11, 12	ltrnel 40395	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝐹) ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊))
53	21, 34, 5, 52	syl3anc 1373	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊))
54	6, 7, 8, 9, 10, 11, 12, 13, 14	cdlemi1 41074	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹)))
55	1, 2, 3, 17, 5, 54	syl221anc 1383	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹)))
56	5, 53, 55	3jca 1128	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊) ∧ ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹))))
57		eqid 2736	. . . . . . 7 ⊢ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
58	6, 7, 8, 9, 10, 11, 12, 13, 57	cdlemh 41073	. . . . . 6 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊) ∧ ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴 ∧ ¬ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ≤ 𝑊))
59	58	simpld 494	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (((𝑈‘𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈‘𝐹)‘𝑃) ≤ 𝑊) ∧ ((𝑈‘𝐹)‘𝑃) ≤ (𝑃 ∨ (𝑅‘𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴)
60	56, 59	syld3an2 1413	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴)
61	7, 10	atcmp 39567	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ ((𝑈‘𝐺)‘𝑃) ∈ 𝐴 ∧ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ∈ 𝐴) → (((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
62	49, 51, 60, 61	syl3anc 1373	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → (((𝑈‘𝐺)‘𝑃) ≤ ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))) ↔ ((𝑈‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))))
63	47, 62	mpbid 232	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹)))))
64		cdlemi.s	. 2 ⊢ 𝑆 = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑈‘𝐹)‘𝑃) ∨ (𝑅‘(𝐺 ∘ ^◡𝐹))))
65	63, 64	eqtr4di 2789	1 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ (𝑈 ∈ 𝐸 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝐹) ≠ (𝑅‘𝐺))) → ((𝑈‘𝐺)‘𝑃) = 𝑆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 class class class wbr 5098 I cid 5518 ^◡ccnv 5623 ↾ cres 5626 ∘ ccom 5628 ‘cfv 6492 (class class class)co 7358 Basecbs 17136 lecple 17184 joincjn 18234 meetcmee 18235 Latclat 18354 Atomscatm 39519 AtLatcal 39520 HLchlt 39606 LHypclh 40240 LTrncltrn 40357 trLctrl 40414 TEndoctendo 41008

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 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-riotaBAD 39209

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-undef 8215 df-map 8765 df-proset 18217 df-poset 18236 df-plt 18251 df-lub 18267 df-glb 18268 df-join 18269 df-meet 18270 df-p0 18346 df-p1 18347 df-lat 18355 df-clat 18422 df-oposet 39432 df-ol 39434 df-oml 39435 df-covers 39522 df-ats 39523 df-atl 39554 df-cvlat 39578 df-hlat 39607 df-llines 39754 df-lplanes 39755 df-lvols 39756 df-lines 39757 df-psubsp 39759 df-pmap 39760 df-padd 40052 df-lhyp 40244 df-laut 40245 df-ldil 40360 df-ltrn 40361 df-trl 40415 df-tendo 41011

This theorem is referenced by: cdlemj1 41077

W3C validator