Theorem cdleml4N

Description: Part of proof of Lemma L of Crawley p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleml1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdleml1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleml1.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdleml1.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	cdleml1.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	cdleml3.o	⊢ 0 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion	cdleml4N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) → ∃ 𝑠 ∈ 𝐸 ( 𝑠 ∘ 𝑈 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		cdleml1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdleml1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		cdleml1.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		cdleml1.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		cdleml1.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6		cdleml3.o	⊢ 0 = ( 𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7	1 2 3	cdlemftr0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑓 ∈ 𝑇 𝑓 ≠ ( I ↾ 𝐵 ) )
8	7	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) → ∃ 𝑓 ∈ 𝑇 𝑓 ≠ ( I ↾ 𝐵 ) )
9		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		simp12l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → 𝑈 ∈ 𝐸 )
11		simp12r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → 𝑉 ∈ 𝐸 )
12		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → 𝑓 ∈ 𝑇 )
13		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → 𝑓 ≠ ( I ↾ 𝐵 ) )
14		simp13l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → 𝑈 ≠ 0 )
15		simp13r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → 𝑉 ≠ 0 )
16	1 2 3 4 5 6	cdleml3N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝑓 ∈ 𝑇 ) ∧ ( 𝑓 ≠ ( I ↾ 𝐵 ) ∧ 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) → ∃ 𝑠 ∈ 𝐸 ( 𝑠 ∘ 𝑈 ) = 𝑉 )
17	9 10 11 12 13 14 15 16	syl133anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) ∧ 𝑓 ∈ 𝑇 ∧ 𝑓 ≠ ( I ↾ 𝐵 ) ) → ∃ 𝑠 ∈ 𝐸 ( 𝑠 ∘ 𝑈 ) = 𝑉 )
18	17	rexlimdv3a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) → ( ∃ 𝑓 ∈ 𝑇 𝑓 ≠ ( I ↾ 𝐵 ) → ∃ 𝑠 ∈ 𝐸 ( 𝑠 ∘ 𝑈 ) = 𝑉 ) )
19	8 18	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) ∧ ( 𝑈 ≠ 0 ∧ 𝑉 ≠ 0 ) ) → ∃ 𝑠 ∈ 𝐸 ( 𝑠 ∘ 𝑈 ) = 𝑉 )