cdlemf

Description: Lemma F in Crawley p. 116. If u is an atom under w, there exists a translation whose trace is u. (Contributed by NM, 12-Apr-2013)

	Ref	Expression
Hypotheses	cdlemf.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemf.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemf.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemf.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemf.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
Assertion	cdlemf	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cdlemf.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemf.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		cdlemf.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		cdlemf.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		cdlemf.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
8	1 6 2 3 7	cdlemf2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) )
9		simp1l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → 𝑝 ∈ 𝐴 )
11		simp3ll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ¬ 𝑝 ≤ 𝑊 )
12		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → 𝑞 ∈ 𝐴 )
13		simp3lr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ¬ 𝑞 ≤ 𝑊 )
14	1 2 3 4	cdleme50ex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑝 ) = 𝑞 )
15	9 10 11 12 13 14	syl122anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑝 ) = 𝑞 )
16		simp3r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → ( 𝑓 ‘ 𝑝 ) = 𝑞 )
17	16	oveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → ( 𝑝 ( join ‘ 𝐾 ) ( 𝑓 ‘ 𝑝 ) ) = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) )
18	17	oveq1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝐾 ) 𝑊 ) = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) )
19		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
20		simp3l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → 𝑓 ∈ 𝑇 )
21		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → 𝑝 ∈ 𝐴 )
22		simp2ll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → ¬ 𝑝 ≤ 𝑊 )
23	1 6 7 2 3 4 5	trlval2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝑓 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
24	19 20 21 22 23	syl112anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → ( 𝑅 ‘ 𝑓 ) = ( ( 𝑝 ( join ‘ 𝐾 ) ( 𝑓 ‘ 𝑝 ) ) ( meet ‘ 𝐾 ) 𝑊 ) )
25		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) )
26	18 24 25	3eqtr4d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ∧ ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) ) → ( 𝑅 ‘ 𝑓 ) = 𝑈 )
27	26	3exp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ) → ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) → ( 𝑅 ‘ 𝑓 ) = 𝑈 ) ) )
28	27	3expia	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) → ( 𝑅 ‘ 𝑓 ) = 𝑈 ) ) ) )
29	28	3imp	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ( ( 𝑓 ∈ 𝑇 ∧ ( 𝑓 ‘ 𝑝 ) = 𝑞 ) → ( 𝑅 ‘ 𝑓 ) = 𝑈 ) )
30	29	expd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ( 𝑓 ∈ 𝑇 → ( ( 𝑓 ‘ 𝑝 ) = 𝑞 → ( 𝑅 ‘ 𝑓 ) = 𝑈 ) ) )
31	30	reximdvai	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ( ∃ 𝑓 ∈ 𝑇 ( 𝑓 ‘ 𝑝 ) = 𝑞 → ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 ) )
32	15 31	mpd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 )
33	32	3exp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 ) ) )
34	33	rexlimdvv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( meet ‘ 𝐾 ) 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 ) )
35	8 34	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 )

Metamath Proof Explorer

Theorem cdlemf

Proof