![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bafval | Structured version Visualization version GIF version |
Description: Value of the function for the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Ref | Expression |
---|---|
bafval.1 | ⊢ 𝑋 = (BaseSet‘𝑈) |
bafval.2 | ⊢ 𝐺 = ( +𝑣 ‘𝑈) |
Ref | Expression |
---|---|
bafval | ⊢ 𝑋 = ran 𝐺 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6842 | . . . . 5 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣 ‘𝑈)) | |
2 | 1 | rneqd 5893 | . . . 4 ⊢ (𝑢 = 𝑈 → ran ( +𝑣 ‘𝑢) = ran ( +𝑣 ‘𝑈)) |
3 | df-ba 29485 | . . . 4 ⊢ BaseSet = (𝑢 ∈ V ↦ ran ( +𝑣 ‘𝑢)) | |
4 | fvex 6855 | . . . . 5 ⊢ ( +𝑣 ‘𝑈) ∈ V | |
5 | 4 | rnex 7848 | . . . 4 ⊢ ran ( +𝑣 ‘𝑈) ∈ V |
6 | 2, 3, 5 | fvmpt 6948 | . . 3 ⊢ (𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈)) |
7 | rn0 5881 | . . . . 5 ⊢ ran ∅ = ∅ | |
8 | 7 | eqcomi 2745 | . . . 4 ⊢ ∅ = ran ∅ |
9 | fvprc 6834 | . . . 4 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ∅) | |
10 | fvprc 6834 | . . . . 5 ⊢ (¬ 𝑈 ∈ V → ( +𝑣 ‘𝑈) = ∅) | |
11 | 10 | rneqd 5893 | . . . 4 ⊢ (¬ 𝑈 ∈ V → ran ( +𝑣 ‘𝑈) = ran ∅) |
12 | 8, 9, 11 | 3eqtr4a 2802 | . . 3 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈)) |
13 | 6, 12 | pm2.61i 182 | . 2 ⊢ (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈) |
14 | bafval.1 | . 2 ⊢ 𝑋 = (BaseSet‘𝑈) | |
15 | bafval.2 | . . 3 ⊢ 𝐺 = ( +𝑣 ‘𝑈) | |
16 | 15 | rneqi 5892 | . 2 ⊢ ran 𝐺 = ran ( +𝑣 ‘𝑈) |
17 | 13, 14, 16 | 3eqtr4i 2774 | 1 ⊢ 𝑋 = ran 𝐺 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1541 ∈ wcel 2106 Vcvv 3445 ∅c0 4282 ran crn 5634 ‘cfv 6496 +𝑣 cpv 29474 BaseSetcba 29475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 ax-un 7671 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-iota 6448 df-fun 6498 df-fv 6504 df-ba 29485 |
This theorem is referenced by: nvi 29503 nvgf 29507 nvsf 29508 nvgcl 29509 nvcom 29510 nvass 29511 nvadd32 29512 nvrcan 29513 nvadd4 29514 nvscl 29515 nvsid 29516 nvsass 29517 nvdi 29519 nvdir 29520 nv2 29521 nvzcl 29523 nv0rid 29524 nv0lid 29525 nv0 29526 nvsz 29527 nvinv 29528 nvinvfval 29529 nvmval 29531 nvmfval 29533 nvnnncan1 29536 nvnegneg 29538 nvrinv 29540 nvlinv 29541 nvaddsub 29544 cnnvba 29568 sspba 29616 isph 29711 phpar 29713 ip0i 29714 ipdirilem 29718 hhba 30056 hhssabloilem 30150 hhshsslem1 30156 |
Copyright terms: Public domain | W3C validator |