Theorem cdlemkvcl

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

	Ref	Expression
Hypotheses	cdlemk.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemk.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemk.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemk.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemk.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemk.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemk.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	cdlemk.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemk.v1	⊢ 𝑉 = ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑋 ‘ 𝑃 ) ) ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) )
Assertion	cdlemkvcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝑉 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cdlemk.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemk.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemk.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemk.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		cdlemk.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		cdlemk.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		cdlemk.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		cdlemk.m	⊢ ∧ = ( meet ‘ 𝐾 )
9		cdlemk.v1	⊢ 𝑉 = ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑋 ‘ 𝑃 ) ) ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) )
10		simp1l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ HL )
11	10	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ Lat )
12		simp1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		simp22	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝐺 ∈ 𝑇 )
14	1 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
15	14	3ad2ant3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
16	1 5 6	ltrncl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐵 )
17	12 13 15 16	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑃 ) ∈ 𝐵 )
18		simp23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝑋 ∈ 𝑇 )
19	1 5 6	ltrncl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑇 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑋 ‘ 𝑃 ) ∈ 𝐵 )
20	12 18 15 19	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ‘ 𝑃 ) ∈ 𝐵 )
21	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝐺 ‘ 𝑃 ) ∈ 𝐵 ∧ ( 𝑋 ‘ 𝑃 ) ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑋 ‘ 𝑃 ) ) ∈ 𝐵 )
22	11 17 20 21	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑋 ‘ 𝑃 ) ) ∈ 𝐵 )
23		simp21	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝐹 ∈ 𝑇 )
24	5 6	ltrncnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ◡ 𝐹 ∈ 𝑇 )
25	12 23 24	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ◡ 𝐹 ∈ 𝑇 )
26	5 6	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
27	12 13 25 26	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 )
28	1 5 6 7	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∘ ◡ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
29	12 27 28	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
30	5 6	ltrnco	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑇 ∧ ◡ 𝐹 ∈ 𝑇 ) → ( 𝑋 ∘ ◡ 𝐹 ) ∈ 𝑇 )
31	12 18 25 30	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∘ ◡ 𝐹 ) ∈ 𝑇 )
32	1 5 6 7	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∘ ◡ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
33	12 31 32	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ∈ 𝐵 )
34	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ∧ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ∈ 𝐵 ) → ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
35	11 29 33 34	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 )
36	1 8	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑋 ‘ 𝑃 ) ) ∈ 𝐵 ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) ∈ 𝐵 ) → ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑋 ‘ 𝑃 ) ) ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐵 )
37	11 22 35 36	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → ( ( ( 𝐺 ‘ 𝑃 ) ∨ ( 𝑋 ‘ 𝑃 ) ) ∧ ( ( 𝑅 ‘ ( 𝐺 ∘ ◡ 𝐹 ) ) ∨ ( 𝑅 ‘ ( 𝑋 ∘ ◡ 𝐹 ) ) ) ) ∈ 𝐵 )
38	9 37	eqeltrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇 ∧ 𝑋 ∈ 𝑇 ) ∧ 𝑃 ∈ 𝐴 ) → 𝑉 ∈ 𝐵 )