| Step | Hyp | Ref
| Expression |
| 1 | | simpl1l 1225 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → 𝐾 ∈ HL) |
| 2 | | hlop 39363 |
. . . . . . 7
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
| 3 | 1, 2 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → 𝐾 ∈ OP) |
| 4 | | simpl1 1192 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 5 | | simpl2r 1228 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → 𝑁 ∈ 𝑇) |
| 6 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 7 | | tendoex.h |
. . . . . . . 8
⊢ 𝐻 = (LHyp‘𝐾) |
| 8 | | tendoex.t |
. . . . . . . 8
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 9 | | tendoex.r |
. . . . . . . 8
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 10 | 6, 7, 8, 9 | trlcl 40166 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑅‘𝑁) ∈ (Base‘𝐾)) |
| 11 | 4, 5, 10 | syl2anc 584 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝑁) ∈ (Base‘𝐾)) |
| 12 | | simpr 484 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝐹) ∈ (Atoms‘𝐾)) |
| 13 | | simpl3 1194 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → (𝑅‘𝑁) ≤ (𝑅‘𝐹)) |
| 14 | | tendoex.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
| 15 | | eqid 2737 |
. . . . . . 7
⊢
(0.‘𝐾) =
(0.‘𝐾) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
| 17 | 6, 14, 15, 16 | leat 39294 |
. . . . . 6
⊢ (((𝐾 ∈ OP ∧ (𝑅‘𝑁) ∈ (Base‘𝐾) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾))) |
| 18 | 3, 11, 12, 13, 17 | syl31anc 1375 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾))) |
| 19 | | simp3 1139 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → (𝑅‘𝑁) ≤ (𝑅‘𝐹)) |
| 20 | | breq2 5147 |
. . . . . . . . 9
⊢ ((𝑅‘𝐹) = (0.‘𝐾) → ((𝑅‘𝑁) ≤ (𝑅‘𝐹) ↔ (𝑅‘𝑁) ≤ (0.‘𝐾))) |
| 21 | 19, 20 | syl5ibcom 245 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝐹) = (0.‘𝐾) → (𝑅‘𝑁) ≤ (0.‘𝐾))) |
| 22 | 21 | imp 406 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝑁) ≤ (0.‘𝐾)) |
| 23 | | simpl1l 1225 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐾 ∈ HL) |
| 24 | 23, 2 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝐾 ∈ OP) |
| 25 | | simpl1 1192 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 26 | | simpl2r 1228 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → 𝑁 ∈ 𝑇) |
| 27 | 25, 26, 10 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝑁) ∈ (Base‘𝐾)) |
| 28 | 6, 14, 15 | ople0 39188 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ (𝑅‘𝑁) ∈ (Base‘𝐾)) → ((𝑅‘𝑁) ≤ (0.‘𝐾) ↔ (𝑅‘𝑁) = (0.‘𝐾))) |
| 29 | 24, 27, 28 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → ((𝑅‘𝑁) ≤ (0.‘𝐾) ↔ (𝑅‘𝑁) = (0.‘𝐾))) |
| 30 | 22, 29 | mpbid 232 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → (𝑅‘𝑁) = (0.‘𝐾)) |
| 31 | 30 | olcd 875 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) ∧ (𝑅‘𝐹) = (0.‘𝐾)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾))) |
| 32 | | simp1 1137 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 33 | | simp2l 1200 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → 𝐹 ∈ 𝑇) |
| 34 | 15, 16, 7, 8, 9 | trlator0 40173 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾))) |
| 35 | 32, 33, 34 | syl2anc 584 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝐹) ∈ (Atoms‘𝐾) ∨ (𝑅‘𝐹) = (0.‘𝐾))) |
| 36 | 18, 31, 35 | mpjaodan 961 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾))) |
| 37 | 36 | 3expa 1119 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾))) |
| 38 | | eqcom 2744 |
. . . . 5
⊢ ((𝑅‘𝑁) = (𝑅‘𝐹) ↔ (𝑅‘𝐹) = (𝑅‘𝑁)) |
| 39 | | tendoex.e |
. . . . . . 7
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
| 40 | 7, 8, 9, 39 | cdlemk 40976 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |
| 41 | 40 | 3expa 1119 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |
| 42 | 38, 41 | sylan2b 594 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (𝑅‘𝐹)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |
| 43 | | eqid 2737 |
. . . . . . 7
⊢ (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) = (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) |
| 44 | 6, 7, 8, 39, 43 | tendo0cl 40792 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸) |
| 45 | 44 | ad2antrr 726 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸) |
| 46 | | simplrl 777 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → 𝐹 ∈ 𝑇) |
| 47 | 43, 6 | tendo02 40789 |
. . . . . . 7
⊢ (𝐹 ∈ 𝑇 → ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = ( I ↾ (Base‘𝐾))) |
| 48 | 46, 47 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = ( I ↾ (Base‘𝐾))) |
| 49 | 6, 15, 7, 8, 9 | trlid0b 40180 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑁 ∈ 𝑇) → (𝑁 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝑁) = (0.‘𝐾))) |
| 50 | 49 | adantrl 716 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) → (𝑁 = ( I ↾ (Base‘𝐾)) ↔ (𝑅‘𝑁) = (0.‘𝐾))) |
| 51 | 50 | biimpar 477 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → 𝑁 = ( I ↾ (Base‘𝐾))) |
| 52 | 48, 51 | eqtr4d 2780 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁) |
| 53 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑢 = (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) → (𝑢‘𝐹) = ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹)) |
| 54 | 53 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑢 = (ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) → ((𝑢‘𝐹) = 𝑁 ↔ ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁)) |
| 55 | 54 | rspcev 3622 |
. . . . 5
⊢ (((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾))) ∈ 𝐸 ∧ ((ℎ ∈ 𝑇 ↦ ( I ↾ (Base‘𝐾)))‘𝐹) = 𝑁) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |
| 56 | 45, 52, 55 | syl2anc 584 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) = (0.‘𝐾)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |
| 57 | 42, 56 | jaodan 960 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ ((𝑅‘𝑁) = (𝑅‘𝐹) ∨ (𝑅‘𝑁) = (0.‘𝐾))) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |
| 58 | 37, 57 | syldan 591 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇)) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |
| 59 | 58 | 3impa 1110 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (𝑅‘𝑁) ≤ (𝑅‘𝐹)) → ∃𝑢 ∈ 𝐸 (𝑢‘𝐹) = 𝑁) |