![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > tendo0cl | Structured version Visualization version GIF version |
Description: The additive identity is a trace-perserving endormorphism. (Contributed by NM, 12-Jun-2013.) |
Ref | Expression |
---|---|
tendo0.b | ⊢ 𝐵 = (Base‘𝐾) |
tendo0.h | ⊢ 𝐻 = (LHyp‘𝐾) |
tendo0.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
tendo0.e | ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
tendo0.o | ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
Ref | Expression |
---|---|
tendo0cl | ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2794 | . 2 ⊢ (le‘𝐾) = (le‘𝐾) | |
2 | tendo0.h | . 2 ⊢ 𝐻 = (LHyp‘𝐾) | |
3 | tendo0.t | . 2 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
4 | eqid 2794 | . 2 ⊢ ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊) | |
5 | tendo0.e | . 2 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) | |
6 | id 22 | . 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
7 | tendo0.b | . . . . 5 ⊢ 𝐵 = (Base‘𝐾) | |
8 | 7, 2, 3 | idltrn 36830 | . . . 4 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇) |
9 | 8 | adantr 481 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑔 ∈ 𝑇) → ( I ↾ 𝐵) ∈ 𝑇) |
10 | tendo0.o | . . . 4 ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) | |
11 | 10 | tendo0cbv 37466 | . . 3 ⊢ 𝑂 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
12 | 9, 11 | fmptd 6744 | . 2 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂:𝑇⟶𝑇) |
13 | 7, 2, 3, 5, 10 | tendo0co2 37468 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑔 ∈ 𝑇 ∧ ℎ ∈ 𝑇) → (𝑂‘(𝑔 ∘ ℎ)) = ((𝑂‘𝑔) ∘ (𝑂‘ℎ))) |
14 | 7, 2, 3, 5, 10, 1, 4 | tendo0tp 37469 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑔 ∈ 𝑇) → (((trL‘𝐾)‘𝑊)‘(𝑂‘𝑔))(le‘𝐾)(((trL‘𝐾)‘𝑊)‘𝑔)) |
15 | 1, 2, 3, 4, 5, 6, 12, 13, 14 | istendod 37442 | 1 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ 𝐸) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2080 ↦ cmpt 5043 I cid 5350 ↾ cres 5448 ‘cfv 6228 Basecbs 16312 lecple 16401 HLchlt 36030 LHypclh 36664 LTrncltrn 36781 trLctrl 36838 TEndoctendo 37432 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-rep 5084 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-riotaBAD 35633 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-ral 3109 df-rex 3110 df-reu 3111 df-rmo 3112 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-iun 4829 df-iin 4830 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-riota 6980 df-ov 7022 df-oprab 7023 df-mpo 7024 df-1st 7548 df-2nd 7549 df-undef 7793 df-map 8261 df-proset 17367 df-poset 17385 df-plt 17397 df-lub 17413 df-glb 17414 df-join 17415 df-meet 17416 df-p0 17478 df-p1 17479 df-lat 17485 df-clat 17547 df-oposet 35856 df-ol 35858 df-oml 35859 df-covers 35946 df-ats 35947 df-atl 35978 df-cvlat 36002 df-hlat 36031 df-llines 36178 df-lplanes 36179 df-lvols 36180 df-lines 36181 df-psubsp 36183 df-pmap 36184 df-padd 36476 df-lhyp 36668 df-laut 36669 df-ldil 36784 df-ltrn 36785 df-trl 36839 df-tendo 37435 |
This theorem is referenced by: tendo0pl 37471 tendo0plr 37472 tendoipl 37477 tendoid0 37505 tendo0mul 37506 tendo0mulr 37507 tendoex 37655 cdleml5N 37660 erngdvlem1 37668 erngdvlem4 37671 erng0g 37674 erngdvlem1-rN 37676 erngdvlem4-rN 37679 dvh0g 37791 dvhopN 37796 dib1dim 37845 dib1dim2 37848 dibss 37849 diblss 37850 diblsmopel 37851 dicn0 37872 cdlemn4 37878 cdlemn4a 37879 cdlemn6 37882 dihopelvalcpre 37928 dihmeetlem4preN 37986 dihatlat 38014 dihatexv 38018 |
Copyright terms: Public domain | W3C validator |