Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. 2
⊢
(le‘𝐾) =
(le‘𝐾) |
2 | | tendoicl.h |
. 2
⊢ 𝐻 = (LHyp‘𝐾) |
3 | | tendoicl.t |
. 2
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
4 | | eqid 2610 |
. 2
⊢
((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊) |
5 | | tendoicl.e |
. 2
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
6 | | simpl 472 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
7 | | simpll 786 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
8 | 2, 3, 5 | tendocl 35073 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → (𝑆‘𝑔) ∈ 𝑇) |
9 | 8 | 3expa 1257 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (𝑆‘𝑔) ∈ 𝑇) |
10 | 2, 3 | ltrncnv 34450 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝑔) ∈ 𝑇) → ◡(𝑆‘𝑔) ∈ 𝑇) |
11 | 7, 9, 10 | syl2anc 691 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → ◡(𝑆‘𝑔) ∈ 𝑇) |
12 | | eqid 2610 |
. . . 4
⊢ (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔)) = (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔)) |
13 | 11, 12 | fmptd 6292 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔)):𝑇⟶𝑇) |
14 | | tendoicl.i |
. . . . . 6
⊢ 𝐼 = (𝑠 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ◡(𝑠‘𝑓))) |
15 | 14, 3 | tendoi 35100 |
. . . . 5
⊢ (𝑆 ∈ 𝐸 → (𝐼‘𝑆) = (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔))) |
16 | 15 | adantl 481 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝐼‘𝑆) = (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔))) |
17 | 16 | feq1d 5943 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → ((𝐼‘𝑆):𝑇⟶𝑇 ↔ (𝑔 ∈ 𝑇 ↦ ◡(𝑆‘𝑔)):𝑇⟶𝑇)) |
18 | 13, 17 | mpbird 246 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝐼‘𝑆):𝑇⟶𝑇) |
19 | | simp1r 1079 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → 𝑆 ∈ 𝐸) |
20 | 2, 3 | ltrnco 35025 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑔 ∘ ℎ) ∈ 𝑇) |
21 | 20 | 3adant1r 1311 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑔 ∘ ℎ) ∈ 𝑇) |
22 | 14, 3 | tendoi2 35101 |
. . . 4
⊢ ((𝑆 ∈ 𝐸 ∧ (𝑔 ∘ ℎ) ∈ 𝑇) → ((𝐼‘𝑆)‘(𝑔 ∘ ℎ)) = ◡(𝑆‘(𝑔 ∘ ℎ))) |
23 | 19, 21, 22 | syl2anc 691 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → ((𝐼‘𝑆)‘(𝑔 ∘ ℎ)) = ◡(𝑆‘(𝑔 ∘ ℎ))) |
24 | | cnvco 5230 |
. . . 4
⊢ ◡((𝑆‘ℎ) ∘ (𝑆‘𝑔)) = (◡(𝑆‘𝑔) ∘ ◡(𝑆‘ℎ)) |
25 | 2, 3 | ltrncom 35044 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑔 ∘ ℎ) = (ℎ ∘ 𝑔)) |
26 | 25 | 3adant1r 1311 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑔 ∘ ℎ) = (ℎ ∘ 𝑔)) |
27 | 26 | fveq2d 6107 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑆‘(𝑔 ∘ ℎ)) = (𝑆‘(ℎ ∘ 𝑔))) |
28 | | simp1ll 1117 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → 𝐾 ∈ HL) |
29 | | simp1lr 1118 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → 𝑊 ∈ 𝐻) |
30 | | simp3 1056 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → ℎ ∈ 𝑇) |
31 | | simp2 1055 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → 𝑔 ∈ 𝑇) |
32 | 2, 3, 5 | tendovalco 35071 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ∧ 𝑆 ∈ 𝐸) ∧ (ℎ ∈ 𝑇 ∧ 𝑔 ∈ 𝑇)) → (𝑆‘(ℎ ∘ 𝑔)) = ((𝑆‘ℎ) ∘ (𝑆‘𝑔))) |
33 | 28, 29, 19, 30, 31, 32 | syl32anc 1326 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑆‘(ℎ ∘ 𝑔)) = ((𝑆‘ℎ) ∘ (𝑆‘𝑔))) |
34 | 27, 33 | eqtrd 2644 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑆‘(𝑔 ∘ ℎ)) = ((𝑆‘ℎ) ∘ (𝑆‘𝑔))) |
35 | 34 | cnveqd 5220 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → ◡(𝑆‘(𝑔 ∘ ℎ)) = ◡((𝑆‘ℎ) ∘ (𝑆‘𝑔))) |
36 | 14, 3 | tendoi2 35101 |
. . . . . 6
⊢ ((𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → ((𝐼‘𝑆)‘𝑔) = ◡(𝑆‘𝑔)) |
37 | 19, 31, 36 | syl2anc 691 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → ((𝐼‘𝑆)‘𝑔) = ◡(𝑆‘𝑔)) |
38 | 14, 3 | tendoi2 35101 |
. . . . . 6
⊢ ((𝑆 ∈ 𝐸 ∧ ℎ ∈ 𝑇) → ((𝐼‘𝑆)‘ℎ) = ◡(𝑆‘ℎ)) |
39 | 19, 30, 38 | syl2anc 691 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → ((𝐼‘𝑆)‘ℎ) = ◡(𝑆‘ℎ)) |
40 | 37, 39 | coeq12d 5208 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (((𝐼‘𝑆)‘𝑔) ∘ ((𝐼‘𝑆)‘ℎ)) = (◡(𝑆‘𝑔) ∘ ◡(𝑆‘ℎ))) |
41 | 24, 35, 40 | 3eqtr4a 2670 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → ◡(𝑆‘(𝑔 ∘ ℎ)) = (((𝐼‘𝑆)‘𝑔) ∘ ((𝐼‘𝑆)‘ℎ))) |
42 | 23, 41 | eqtrd 2644 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → ((𝐼‘𝑆)‘(𝑔 ∘ ℎ)) = (((𝐼‘𝑆)‘𝑔) ∘ ((𝐼‘𝑆)‘ℎ))) |
43 | 36 | adantll 746 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → ((𝐼‘𝑆)‘𝑔) = ◡(𝑆‘𝑔)) |
44 | 43 | fveq2d 6107 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘((𝐼‘𝑆)‘𝑔)) = (((trL‘𝐾)‘𝑊)‘◡(𝑆‘𝑔))) |
45 | 2, 3, 4 | trlcnv 34470 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆‘𝑔) ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘◡(𝑆‘𝑔)) = (((trL‘𝐾)‘𝑊)‘(𝑆‘𝑔))) |
46 | 7, 9, 45 | syl2anc 691 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘◡(𝑆‘𝑔)) = (((trL‘𝐾)‘𝑊)‘(𝑆‘𝑔))) |
47 | 44, 46 | eqtrd 2644 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘((𝐼‘𝑆)‘𝑔)) = (((trL‘𝐾)‘𝑊)‘(𝑆‘𝑔))) |
48 | 1, 2, 3, 4, 5 | tendotp 35067 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘(𝑆‘𝑔))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔)) |
49 | 48 | 3expa 1257 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘(𝑆‘𝑔))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔)) |
50 | 47, 49 | eqbrtrd 4605 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘((𝐼‘𝑆)‘𝑔))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔)) |
51 | 1, 2, 3, 4, 5, 6, 18, 42, 50 | istendod 35068 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → (𝐼‘𝑆) ∈ 𝐸) |