Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
⊢
(le‘𝐾) =
(le‘𝐾) |
2 | | tendopl.h |
. 2
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | tendopl.t |
. 2
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
4 | | eqid 2622 |
. 2
⊢
((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊) |
5 | | tendopl.e |
. 2
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
6 | | simp1 1061 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
7 | | simpl1 1064 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
8 | | simpl2 1065 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → 𝑈 ∈ 𝐸) |
9 | | simpr 477 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → 𝑔 ∈ 𝑇) |
10 | 2, 3, 5 | tendocl 36055 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → (𝑈‘𝑔) ∈ 𝑇) |
11 | 7, 8, 9, 10 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (𝑈‘𝑔) ∈ 𝑇) |
12 | | simpl3 1066 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → 𝑉 ∈ 𝐸) |
13 | 2, 3, 5 | tendocl 36055 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑉 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → (𝑉‘𝑔) ∈ 𝑇) |
14 | 7, 12, 9, 13 | syl3anc 1326 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (𝑉‘𝑔) ∈ 𝑇) |
15 | 2, 3 | ltrnco 36007 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈‘𝑔) ∈ 𝑇 ∧ (𝑉‘𝑔) ∈ 𝑇) → ((𝑈‘𝑔) ∘ (𝑉‘𝑔)) ∈ 𝑇) |
16 | 7, 11, 14, 15 | syl3anc 1326 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → ((𝑈‘𝑔) ∘ (𝑉‘𝑔)) ∈ 𝑇) |
17 | | eqid 2622 |
. . . 4
⊢ (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔))) = (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔))) |
18 | 16, 17 | fmptd 6385 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔))):𝑇⟶𝑇) |
19 | | tendopl.p |
. . . . . 6
⊢ 𝑃 = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) |
20 | 19, 3 | tendopl 36064 |
. . . . 5
⊢ ((𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) = (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔)))) |
21 | 20 | 3adant1 1079 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) = (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔)))) |
22 | 21 | feq1d 6030 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → ((𝑈𝑃𝑉):𝑇⟶𝑇 ↔ (𝑔 ∈ 𝑇 ↦ ((𝑈‘𝑔) ∘ (𝑉‘𝑔))):𝑇⟶𝑇)) |
23 | 18, 22 | mpbird 247 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉):𝑇⟶𝑇) |
24 | | simp11 1091 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇 ∧ 𝑖 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
25 | | simp12 1092 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇 ∧ 𝑖 ∈ 𝑇) → 𝑈 ∈ 𝐸) |
26 | | simp13 1093 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇 ∧ 𝑖 ∈ 𝑇) → 𝑉 ∈ 𝐸) |
27 | | 3simpc 1060 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇 ∧ 𝑖 ∈ 𝑇) → (ℎ ∈ 𝑇 ∧ 𝑖 ∈ 𝑇)) |
28 | 2, 3, 5, 19 | tendoplco2 36067 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ (ℎ ∈ 𝑇 ∧ 𝑖 ∈ 𝑇)) → ((𝑈𝑃𝑉)‘(ℎ ∘ 𝑖)) = (((𝑈𝑃𝑉)‘ℎ) ∘ ((𝑈𝑃𝑉)‘𝑖))) |
29 | 24, 25, 26, 27, 28 | syl121anc 1331 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇 ∧ 𝑖 ∈ 𝑇) → ((𝑈𝑃𝑉)‘(ℎ ∘ 𝑖)) = (((𝑈𝑃𝑉)‘ℎ) ∘ ((𝑈𝑃𝑉)‘𝑖))) |
30 | | simpl1 1064 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
31 | | simpl2 1065 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇) → 𝑈 ∈ 𝐸) |
32 | | simpl3 1066 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇) → 𝑉 ∈ 𝐸) |
33 | | simpr 477 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇) → ℎ ∈ 𝑇) |
34 | 2, 3, 5, 19, 1, 4 | tendopltp 36068 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘((𝑈𝑃𝑉)‘ℎ))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘ℎ)) |
35 | 30, 31, 32, 33, 34 | syl121anc 1331 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) ∧ ℎ ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘((𝑈𝑃𝑉)‘ℎ))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘ℎ)) |
36 | 1, 2, 3, 4, 5, 6, 23, 29, 35 | istendod 36050 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸) → (𝑈𝑃𝑉) ∈ 𝐸) |