Theorem cdlemi

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

	Ref	Expression
Hypotheses	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	cdlemi	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) = 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		cdlemi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemi.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemi.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemi.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdlemi.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdlemi.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		cdlemi.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8		cdlemi.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9		cdlemi.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
10		cdlemi.s	⊢ 𝑆 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
11		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL )
12		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑊 ∈ 𝐻 )
13		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑈 ∈ 𝐸 )
14		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 )
15		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
16	1 2 3 4 5 6 7 8 9	cdlemi1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )
17	11 12 13 14 15 16	syl221anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) )
18		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 )
19	1 2 3 4 5 6 7 8 9	cdlemi2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
20	11 12 13 18 14 15 19	syl231anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
21	11	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ Lat )
22		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23	6 7 9	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝐺 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 )
24	22 13 14 23	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 )
25		simp2rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐴 )
26	1 5	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
27	25 26	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐵 )
28	1 6 7	ltrncl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 )
29	22 24 27 28	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 )
30	1 6 7 8	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
31	22 14 30	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
32	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
33	21 27 31 32	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
34	6 7 9	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 )
35	22 13 18 34	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 )
36	1 6 7	ltrncl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐵 )
37	22 35 27 36	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐵 )
38	6 7	ltrncnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 )
39	22 18 38	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ◡ 𝐹 ∈ 𝑇 )
40	6 7	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
41	22 14 39 40	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
42	1 6 7 8	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
43	22 41 42	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
44	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ) → ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
45	21 37 43 44	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
46	1 2 4	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐵 ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 ) ) → ( ( ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ↔ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ) )
47	21 29 33 45 46	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ↔ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ) )
48	17 20 47	mpbi2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
49		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
50	11 49	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ AtLat )
51	2 5 6 7	ltrnat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐺 ) ∈ 𝑇 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐴 )
52	22 24 25 51	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐴 )
53	2 5 6 7	ltrnel	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ‘ 𝐹 ) ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ 𝑊 ) )
54	22 35 15 53	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ 𝑊 ) )
55	1 2 3 4 5 6 7 8 9	cdlemi1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) )
56	11 12 13 18 15 55	syl221anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) )
57	15 54 56	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ 𝑊 ) ∧ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) )
58		eqid	⊢ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) )
59	1 2 3 4 5 6 7 8 58	cdlemh	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ 𝑊 ) ∧ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 ∧ ¬ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ≤ 𝑊 ) )
60	59	simpld	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ 𝑊 ) ∧ ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 )
61	57 60	syld3an2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 )
62	2 5	atcmp	⊢ ( ( 𝐾 ∈ AtLat ∧ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ∈ 𝐴 ∧ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐴 ) → ( ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ↔ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ) )
63	50 52 61 62	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ↔ ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) ) )
64	48 63	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( ( ( 𝑈 ‘ 𝐹 ) ‘ 𝑃 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ) ) )
65	64 10	eqtr4di	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑈 ∈ 𝐸 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝐹 ≠ ( I ↾ 𝐵 ) ∧ 𝐺 ≠ ( I ↾ 𝐵 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑈 ‘ 𝐺 ) ‘ 𝑃 ) = 𝑆 )