Theorem cdlemfnid

Description: cdlemf with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemfnid.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemfnid.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemfnid.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		cdlemfnid.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		cdlemfnid.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6		cdlemfnid.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
7	2 3 4 5 6	cdlemf	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 )
8		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → ( 𝑅 ‘ 𝑓 ) = 𝑈 )
9		simp1rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → 𝑈 ∈ 𝐴 )
10	8 9	eqeltrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → ( 𝑅 ‘ 𝑓 ) ∈ 𝐴 )
11		simp1l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → 𝑓 ∈ 𝑇 )
13	1 3 4 5 6	trlnidatb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝑓 ) ∈ 𝐴 ) )
14	11 12 13	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → ( 𝑓 ≠ ( I ↾ 𝐵 ) ↔ ( 𝑅 ‘ 𝑓 ) ∈ 𝐴 ) )
15	10 14	mpbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → 𝑓 ≠ ( I ↾ 𝐵 ) )
16	8 15	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝑓 ) = 𝑈 ) → ( ( 𝑅 ‘ 𝑓 ) = 𝑈 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) )
17	16	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ 𝑓 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝑓 ) = 𝑈 → ( ( 𝑅 ‘ 𝑓 ) = 𝑈 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ) )
18	17	reximdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( ∃ 𝑓 ∈ 𝑇 ( 𝑅 ‘ 𝑓 ) = 𝑈 → ∃ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) = 𝑈 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) ) )
19	7 18	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑓 ∈ 𝑇 ( ( 𝑅 ‘ 𝑓 ) = 𝑈 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) )