cdlemg35

Description: TODO: Fix comment. TODO: should we have a more general version of hlsupr to avoid the =/= conditions? (Contributed by NM, 31-May-2013)

	Ref	Expression
Hypotheses	cdlemg35.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemg35.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemg35.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemg35.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemg35.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemg35.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemg35.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	cdlemg35	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ≤ 𝑊 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemg35.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemg35.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemg35.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cdlemg35.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemg35.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemg35.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemg35.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL )
9		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		simp21	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
11		simp22	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 )
12		simp31	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 )
13	1 4 5 6 7	trlat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
14	9 10 11 12 13	syl112anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
15		simp23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 )
16		simp32	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 )
17	1 4 5 6 7	trlat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐺 ∈ 𝑇 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 )
18	9 10 15 16 17	syl112anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 )
19		simp33	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
20	1 2 4	hlsupr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
21	8 14 18 19 20	syl31anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) )
22		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
23		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝐾 ∈ HL )
24	23	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝐾 ∈ Lat )
25	22 4	atbase	⊢ ( 𝑣 ∈ 𝐴 → 𝑣 ∈ ( Base ‘ 𝐾 ) )
26	25	3ad2ant2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝑣 ∈ ( Base ‘ 𝐾 ) )
27		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
28		simp122	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝐹 ∈ 𝑇 )
29	22 5 6 7	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
30	27 28 29	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) )
31		simp123	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝐺 ∈ 𝑇 )
32	22 5 6 7	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
33	27 31 32	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
34	22 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
35	24 30 33 34	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ ( Base ‘ 𝐾 ) )
36		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝑊 ∈ 𝐻 )
37	22 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
38	36 37	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
39		simp33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) )
40	1 5 6 7	trlle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
41	27 28 40	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 )
42	1 5 6 7	trlle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ≤ 𝑊 )
43	27 31 42	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( 𝑅 ‘ 𝐺 ) ≤ 𝑊 )
44	22 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 ∧ ( 𝑅 ‘ 𝐺 ) ≤ 𝑊 ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ≤ 𝑊 ) )
45	24 30 33 38 44	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( ( ( 𝑅 ‘ 𝐹 ) ≤ 𝑊 ∧ ( 𝑅 ‘ 𝐺 ) ≤ 𝑊 ) ↔ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ≤ 𝑊 ) )
46	41 43 45	mpbi2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ≤ 𝑊 )
47	22 1 24 26 35 38 39 46	lattrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝑣 ≤ 𝑊 )
48		simp31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) )
49		simp32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) )
50	47 48 49	jca32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) ) → ( 𝑣 ≤ 𝑊 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ) ) )
51	50	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) ∧ 𝑣 ∈ 𝐴 ) → ( ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑣 ≤ 𝑊 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ) ) ) )
52	51	reximdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ∃ 𝑣 ∈ 𝐴 ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ∧ 𝑣 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝐺 ) ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ≤ 𝑊 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ) ) ) )
53	21 52	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝐺 ‘ 𝑃 ) ≠ 𝑃 ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑣 ≤ 𝑊 ∧ ( 𝑣 ≠ ( 𝑅 ‘ 𝐹 ) ∧ 𝑣 ≠ ( 𝑅 ‘ 𝐺 ) ) ) )

Metamath Proof Explorer

Theorem cdlemg35

Proof