cdlemh1

Description: Part of proof of Lemma H of Crawley p. 118. (Contributed by NM, 17-Jun-2013)

	Ref	Expression
Hypotheses	cdlemh.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemh.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemh.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemh.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemh.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemh.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemh.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemh.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	cdlemh.s	⊢ 𝑆 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
Assertion	cdlemh1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemh.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemh.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemh.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemh.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdlemh.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdlemh.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		cdlemh.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8		cdlemh.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9		cdlemh.s	⊢ 𝑆 = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
10	9	oveq1i	⊢ ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) )
11		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ HL )
12		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝑇 )
14		simp12	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐹 ∈ 𝑇 )
15		simp3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) )
16	15	necomd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) )
17	5 6 7 8	trlcocnvat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝐹 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐺 ) ≠ ( 𝑅 ‘ 𝐹 ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐴 )
18	12 13 14 16 17	syl121anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐴 )
19	11	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝐾 ∈ Lat )
20		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐴 )
21	1 5	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
22	20 21	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑃 ∈ 𝐵 )
23	1 6 7 8	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
24	12 13 23	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 )
25	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
26	19 22 24 25	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 )
27		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ∈ 𝐴 )
28	1 3 5	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐴 ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∈ 𝐵 )
29	11 27 18 28	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∈ 𝐵 )
30	2 3 5	hlatlej2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐴 ) → ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
31	11 27 18 30	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
32	1 2 3 4 5	atmod4i1	⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐴 ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∈ 𝐵 ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∈ 𝐵 ) ∧ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ≤ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
33	11 18 26 29 31 32	syl131anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
34	6 7	ltrncnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ^◡ 𝐹 ∈ 𝑇 )
35	12 14 34	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ^◡ 𝐹 ∈ 𝑇 )
36	3 6 7 8	trljco2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ^◡ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ ^◡ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
37	12 13 35 36	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ ^◡ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
38	6 7 8	trlcnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ ^◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
39	12 14 38	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ^◡ 𝐹 ) = ( 𝑅 ‘ 𝐹 ) )
40	39	oveq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ ^◡ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
41	37 40	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
42	41	oveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
43	6 7	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ^◡ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ ^◡ 𝐹 ) ∈ 𝑇 )
44	12 13 35 43	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝐺 ∘ ^◡ 𝐹 ) ∈ 𝑇 )
45	1 6 7 8	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ^◡ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐵 )
46	12 44 45	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐵 )
47	1 3	latjass	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐵 ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
48	19 22 24 46 47	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐺 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
49	1 6 7 8	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 )
50	12 14 49	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 )
51	1 3	latjass	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐵 ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
52	19 22 50 46 51	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( 𝑃 ∨ ( ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
53	42 48 52	3eqtr4d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
54	53	oveq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) = ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
55		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) )
56	1 5	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
57	27 56	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → 𝑄 ∈ 𝐵 )
58	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 )
59	19 22 50 58	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 )
60	1 2 3	latjlej1	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐵 ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐵 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
61	19 57 59 46 60	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
62	55 61	mpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
63	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ∈ 𝐵 ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∈ 𝐵 )
64	19 59 46 63	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∈ 𝐵 )
65	1 2 4	latleeqm2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∈ 𝐵 ∧ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∈ 𝐵 ) → ( ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ↔ ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
66	19 29 64 65	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ≤ ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ↔ ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) )
67	62 66	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
68	33 54 67	3eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( ( ( 𝑃 ∨ ( 𝑅 ‘ 𝐺 ) ) ∧ ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) ) ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )
69	10 68	eqtrid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑄 ≤ ( 𝑃 ∨ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ ( 𝑅 ‘ 𝐺 ) ) ) → ( 𝑆 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) = ( 𝑄 ∨ ( 𝑅 ‘ ( 𝐺 ∘ ^◡ 𝐹 ) ) ) )

Metamath Proof Explorer

Theorem cdlemh1

Proof