Metamath Proof Explorer

Theorem tendoex

Description: Generalization of Lemma K of Crawley p. 118, cdlemk . TODO: can this be used to shorten uses of cdlemk ? (Contributed by NM, 15-Oct-2013)

Ref Expression
Hypotheses tendoex.l ⊢ ≤ = ( le ‘ 𝐾 )
tendoex.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
tendoex.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tendoex.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
tendoex.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendoex ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 tendoex.l ⊢ ≤ = ( le ‘ 𝐾 )
2 tendoex.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 tendoex.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 tendoex.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5 tendoex.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
6 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ HL )
7 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8 6 7 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP )
9 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → 𝑁 ∈ 𝑇 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 2 3 4 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑁 ∈ 𝑇 ) → ( 𝑅 ‘ 𝑁 ) ∈ ( Base ‘ 𝐾 ) )
13 9 10 12 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑁 ) ∈ ( Base ‘ 𝐾 ) )
14 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) )
15 simpl3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) )
16 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
17 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
18 11 1 16 17 leat ⊢ ( ( ( 𝐾 ∈ OP ∧ ( 𝑅 ‘ 𝑁 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
19 8 13 14 15 18 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
20 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) )
21 breq2 ⊢ ( ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) → ( ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝑁 ) ≤ ( 0. ‘ 𝐾 ) ) )
22 20 21 syl5ibcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) → ( 𝑅 ‘ 𝑁 ) ≤ ( 0. ‘ 𝐾 ) ) )
23 22 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑁 ) ≤ ( 0. ‘ 𝐾 ) )
24 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐾 ∈ HL )
25 24 7 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝐾 ∈ OP )
26 simpl1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
27 simpl2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → 𝑁 ∈ 𝑇 )
28 26 27 12 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑁 ) ∈ ( Base ‘ 𝐾 ) )
29 11 1 16 ople0 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑅 ‘ 𝑁 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝑁 ) ≤ ( 0. ‘ 𝐾 ) ↔ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
30 25 28 29 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝑁 ) ≤ ( 0. ‘ 𝐾 ) ↔ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
31 23 30 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) )
32 31 olcd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) → ( ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
33 simp1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
34 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → 𝐹 ∈ 𝑇 )
35 16 17 2 3 4 trlator0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∨ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
36 33 34 35 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( ( 𝑅 ‘ 𝐹 ) ∈ ( Atoms ‘ 𝐾 ) ∨ ( 𝑅 ‘ 𝐹 ) = ( 0. ‘ 𝐾 ) ) )
37 19 32 36 mpjaodan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
38 37 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ( ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
39 eqcom ⊢ ( ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ↔ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) )
40 2 3 4 5 cdlemk ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )
41 40 3expa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝐹 ) = ( 𝑅 ‘ 𝑁 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )
42 39 41 sylan2b ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )
43 eqid ⊢ ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
44 11 2 3 5 43 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ 𝐸 )
45 44 ad2antrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) → ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ 𝐸 )
46 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) → 𝐹 ∈ 𝑇 )
47 43 11 tendo02 ⊢ ( 𝐹 ∈ 𝑇 → ( ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ‘ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
48 46 47 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) → ( ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ‘ 𝐹 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
49 11 16 2 3 4 trlid0b ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑁 ∈ 𝑇 ) → ( 𝑁 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
50 49 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) → ( 𝑁 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) )
51 50 biimpar ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) → 𝑁 = ( I ↾ ( Base ‘ 𝐾 ) ) )
52 48 51 eqtr4d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) → ( ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ‘ 𝐹 ) = 𝑁 )
53 fveq1 ⊢ ( 𝑢 = ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( 𝑢 ‘ 𝐹 ) = ( ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ‘ 𝐹 ) )
54 53 eqeq1d ⊢ ( 𝑢 = ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑢 ‘ 𝐹 ) = 𝑁 ↔ ( ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ‘ 𝐹 ) = 𝑁 ) )
55 54 rspcev ⊢ ( ( ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ∈ 𝐸 ∧ ( ( ℎ ∈ 𝑇 ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) ‘ 𝐹 ) = 𝑁 ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )
56 45 52 55 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )
57 42 56 jaodan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝐹 ) ∨ ( 𝑅 ‘ 𝑁 ) = ( 0. ‘ 𝐾 ) ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )
58 38 57 syldan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )
59 58 3impa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ) ∧ ( 𝑅 ‘ 𝑁 ) ≤ ( 𝑅 ‘ 𝐹 ) ) → ∃ 𝑢 ∈ 𝐸 ( 𝑢 ‘ 𝐹 ) = 𝑁 )