![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > tendocl | Structured version Visualization version GIF version |
Description: Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
Ref | Expression |
---|---|
tendof.h | ⊢ 𝐻 = (LHyp‘𝐾) |
tendof.t | ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
tendof.e | ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
tendocl | ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑆‘𝐹) ∈ 𝑇) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tendof.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | tendof.t | . . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) | |
3 | tendof.e | . . . 4 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) | |
4 | 1, 2, 3 | tendof 37451 | . . 3 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸) → 𝑆:𝑇⟶𝑇) |
5 | 4 | 3adant3 1125 | . 2 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → 𝑆:𝑇⟶𝑇) |
6 | simp3 1131 | . 2 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ 𝑇) | |
7 | 5, 6 | ffvelrnd 6724 | 1 ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇) → (𝑆‘𝐹) ∈ 𝑇) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1080 = wceq 1525 ∈ wcel 2083 ⟶wf 6228 ‘cfv 6232 LHypclh 36672 LTrncltrn 36789 TEndoctendo 37440 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-oprab 7027 df-mpo 7028 df-map 8265 df-tendo 37443 |
This theorem is referenced by: tendoco2 37456 tendococl 37460 tendoid 37461 tendoplcl2 37466 tendopltp 37468 tendoplcl 37469 tendoplcom 37470 tendodi1 37472 tendodi2 37473 tendo0pl 37479 tendoicl 37484 tendoipl 37485 cdlemi1 37506 cdlemi2 37507 cdlemi 37508 cdlemj2 37510 tendo0mul 37514 tendoconid 37517 tendotr 37518 cdleml1N 37664 cdleml2N 37665 cdleml6 37669 dva1dim 37673 tendospcl 37706 tendocnv 37709 tendospcanN 37711 dvalveclem 37713 dialss 37734 dvhvscacl 37791 dvhlveclem 37796 dib1dim 37853 dib1dim2 37856 diblss 37858 dicssdvh 37874 diclspsn 37882 cdlemn6 37890 dihopelvalcpre 37936 dih1 37974 dihglbcpreN 37988 dih1dimatlem0 38016 dih1dimatlem 38017 |
Copyright terms: Public domain | W3C validator |