| Step | Hyp | Ref
| Expression |
| 1 | | tendoset.e |
. 2
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
| 2 | | tendoset.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
| 3 | | tendoset.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | 2, 3 | tendofset 40760 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (TEndo‘𝐾) = (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})) |
| 5 | 4 | fveq1d 6908 |
. . 3
⊢ (𝐾 ∈ 𝑉 → ((TEndo‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊)) |
| 6 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
| 7 | 6, 6 | feq23d 6731 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ↔ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊))) |
| 8 | 6 | raleqdv 3326 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)))) |
| 9 | 6, 8 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)))) |
| 10 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = ((trL‘𝐾)‘𝑊)) |
| 11 | | tendoset.r |
. . . . . . . . . . 11
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 12 | 10, 11 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = 𝑅) |
| 13 | 12 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) = (𝑅‘(𝑠‘𝑓))) |
| 14 | 12 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘𝑓) = (𝑅‘𝑓)) |
| 15 | 13, 14 | breq12d 5156 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓) ↔ (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))) |
| 16 | 6, 15 | raleqbidv 3346 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))) |
| 17 | 7, 9, 16 | 3anbi123d 1438 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓)) ↔ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)))) |
| 18 | 17 | abbidv 2808 |
. . . . 5
⊢ (𝑤 = 𝑊 → {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))} = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}) |
| 19 | | eqid 2737 |
. . . . 5
⊢ (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))}) = (𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))}) |
| 20 | | fvex 6919 |
. . . . . . . 8
⊢
((LTrn‘𝐾)‘𝑊) ∈ V |
| 21 | 20, 20 | mapval 8878 |
. . . . . . 7
⊢
(((LTrn‘𝐾)‘𝑊) ↑m ((LTrn‘𝐾)‘𝑊)) = {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)} |
| 22 | | ovex 7464 |
. . . . . . 7
⊢
(((LTrn‘𝐾)‘𝑊) ↑m ((LTrn‘𝐾)‘𝑊)) ∈ V |
| 23 | 21, 22 | eqeltrri 2838 |
. . . . . 6
⊢ {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)} ∈ V |
| 24 | | simp1 1137 |
. . . . . . 7
⊢ ((𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)) → 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)) |
| 25 | 24 | ss2abi 4067 |
. . . . . 6
⊢ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} ⊆ {𝑠 ∣ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)} |
| 26 | 23, 25 | ssexi 5322 |
. . . . 5
⊢ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} ∈ V |
| 27 | 18, 19, 26 | fvmpt 7016 |
. . . 4
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊) = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}) |
| 28 | | tendoset.t |
. . . . . . 7
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 29 | 28, 28 | feq23i 6730 |
. . . . . 6
⊢ (𝑠:𝑇⟶𝑇 ↔ 𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊)) |
| 30 | 28 | raleqi 3324 |
. . . . . . 7
⊢
(∀𝑔 ∈
𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔))) |
| 31 | 28, 30 | raleqbii 3344 |
. . . . . 6
⊢
(∀𝑓 ∈
𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔))) |
| 32 | 28 | raleqi 3324 |
. . . . . 6
⊢
(∀𝑓 ∈
𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓) ↔ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)) |
| 33 | 29, 31, 32 | 3anbi123i 1156 |
. . . . 5
⊢ ((𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓)) ↔ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))) |
| 34 | 33 | abbii 2809 |
. . . 4
⊢ {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} = {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑊)⟶((LTrn‘𝐾)‘𝑊) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))} |
| 35 | 27, 34 | eqtr4di 2795 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ {𝑠 ∣ (𝑠:((LTrn‘𝐾)‘𝑤)⟶((LTrn‘𝐾)‘𝑤) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)∀𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ ((LTrn‘𝐾)‘𝑤)(((trL‘𝐾)‘𝑤)‘(𝑠‘𝑓)) ≤ (((trL‘𝐾)‘𝑤)‘𝑓))})‘𝑊) = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}) |
| 36 | 5, 35 | sylan9eq 2797 |
. 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → ((TEndo‘𝐾)‘𝑊) = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}) |
| 37 | 1, 36 | eqtrid 2789 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐸 = {𝑠 ∣ (𝑠:𝑇⟶𝑇 ∧ ∀𝑓 ∈ 𝑇 ∀𝑔 ∈ 𝑇 (𝑠‘(𝑓 ∘ 𝑔)) = ((𝑠‘𝑓) ∘ (𝑠‘𝑔)) ∧ ∀𝑓 ∈ 𝑇 (𝑅‘(𝑠‘𝑓)) ≤ (𝑅‘𝑓))}) |