Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imasvscafn Unicode version

Theorem imasvscafn 13538
 Description: The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
imasvscaf.u s
imasvscaf.v
imasvscaf.f
imasvscaf.r
imasvscaf.g Scalar
imasvscaf.k
imasvscaf.q
imasvscaf.s
imasvscaf.e
Assertion
Ref Expression
imasvscafn
Distinct variable groups:   ,,,   ,,,   ,,,   ,,   ,,   ,,   ,,,   ,,,
Allowed substitution hints:   ()   ()   ()   (,,)   (,,)   (,,)

Proof of Theorem imasvscafn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2358 . . . . . . . 8
2 fvex 5622 . . . . . . . 8
31, 2fnmpt2i 6280 . . . . . . 7
4 fnrel 5424 . . . . . . 7
53, 4ax-mp 8 . . . . . 6
65rgenw 2686 . . . . 5
7 reliun 4888 . . . . 5
86, 7mpbir 200 . . . 4
9 imasvscaf.u . . . . . 6 s
10 imasvscaf.v . . . . . 6
11 imasvscaf.f . . . . . 6
12 imasvscaf.r . . . . . 6
13 imasvscaf.g . . . . . 6 Scalar
14 imasvscaf.k . . . . . 6
15 imasvscaf.q . . . . . 6
16 imasvscaf.s . . . . . 6
179, 10, 11, 12, 13, 14, 15, 16imasvsca 13522 . . . . 5
1817releqd 4855 . . . 4
198, 18mpbiri 224 . . 3
20 dffn2 5473 . . . . . . . . . . . . 13
213, 20mpbi 199 . . . . . . . . . . . 12
22 fssxp 5483 . . . . . . . . . . . 12
2321, 22ax-mp 8 . . . . . . . . . . 11
24 fof 5534 . . . . . . . . . . . . . . 15
2511, 24syl 15 . . . . . . . . . . . . . 14
26 ffvelrn 5746 . . . . . . . . . . . . . 14
2725, 26sylan 457 . . . . . . . . . . . . 13
2827snssd 3839 . . . . . . . . . . . 12
29 xpss2 4878 . . . . . . . . . . . 12
30 xpss1 4877 . . . . . . . . . . . 12
3128, 29, 303syl 18 . . . . . . . . . . 11
3223, 31syl5ss 3266 . . . . . . . . . 10
3332ralrimiva 2702 . . . . . . . . 9
34 iunss 4024 . . . . . . . . 9
3533, 34sylibr 203 . . . . . . . 8
3617, 35eqsstrd 3288 . . . . . . 7
37 dmss 4960 . . . . . . 7
3836, 37syl 15 . . . . . 6
39 vn0 3538 . . . . . . 7
40 dmxp 4979 . . . . . . 7
4139, 40ax-mp 8 . . . . . 6
4238, 41syl6sseq 3300 . . . . 5
43 forn 5537 . . . . . . 7
4411, 43syl 15 . . . . . 6
4544xpeq2d 4795 . . . . 5
4642, 45sseqtr4d 3291 . . . 4
47 df-br 4105 . . . . . . . . . 10
4817eleq2d 2425 . . . . . . . . . . . 12
4948adantr 451 . . . . . . . . . . 11
50 eliun 3990 . . . . . . . . . . . 12
51 df-3an 936 . . . . . . . . . . . . . . 15
521mpt2fun 6033 . . . . . . . . . . . . . . . . . . . 20
53 funopfv 5645 . . . . . . . . . . . . . . . . . . . 20
5452, 53ax-mp 8 . . . . . . . . . . . . . . . . . . 19
55 df-ov 5948 . . . . . . . . . . . . . . . . . . . 20
56 opex 4319 . . . . . . . . . . . . . . . . . . . . . . . 24
57 vex 2867 . . . . . . . . . . . . . . . . . . . . . . . 24
5856, 57opeldm 4964 . . . . . . . . . . . . . . . . . . . . . . 23
591, 2dmmpt2 6281 . . . . . . . . . . . . . . . . . . . . . . 23
6058, 59syl6eleq 2448 . . . . . . . . . . . . . . . . . . . . . 22
61 opelxp 4801 . . . . . . . . . . . . . . . . . . . . . 22
6260, 61sylib 188 . . . . . . . . . . . . . . . . . . . . 21
63 oveq1 5952 . . . . . . . . . . . . . . . . . . . . . . 23
6463fveq2d 5612 . . . . . . . . . . . . . . . . . . . . . 22
65 eqidd 2359 . . . . . . . . . . . . . . . . . . . . . 22
6664eqcoms 2361 . . . . . . . . . . . . . . . . . . . . . . . 24
6766eqcomd 2363 . . . . . . . . . . . . . . . . . . . . . . 23
68 eqidd 2359 . . . . . . . . . . . . . . . . . . . . . . 23
6967, 68cbvmpt2v 6013 . . . . . . . . . . . . . . . . . . . . . 22
7064, 65, 69, 2ovmpt2 6070 . . . . . . . . . . . . . . . . . . . . 21
7162, 70syl 15 . . . . . . . . . . . . . . . . . . . 20
7255, 71syl5eqr 2404 . . . . . . . . . . . . . . . . . . 19
7354, 72eqtr3d 2392 . . . . . . . . . . . . . . . . . 18
7473adantl 452 . . . . . . . . . . . . . . . . 17
7562simprd 449 . . . . . . . . . . . . . . . . . . 19
76 elsni 3740 . . . . . . . . . . . . . . . . . . 19
7775, 76syl 15 . . . . . . . . . . . . . . . . . 18
78 imasvscaf.e . . . . . . . . . . . . . . . . . . 19
7978imp 418 . . . . . . . . . . . . . . . . . 18
8077, 79sylan2 460 . . . . . . . . . . . . . . . . 17
8174, 80eqtr4d 2393 . . . . . . . . . . . . . . . 16
8281ex 423 . . . . . . . . . . . . . . 15
8351, 82sylan2br 462 . . . . . . . . . . . . . 14
8483anassrs 629 . . . . . . . . . . . . 13
8584rexlimdva 2743 . . . . . . . . . . . 12
8650, 85syl5bi 208 . . . . . . . . . . 11
8749, 86sylbid 206 . . . . . . . . . 10
8847, 87syl5bi 208 . . . . . . . . 9
8988alrimiv 1631 . . . . . . . 8
90 mo2icl 3020 . . . . . . . 8
9189, 90syl 15 . . . . . . 7
9291ralrimivva 2711 . . . . . 6
93 fofn 5536 . . . . . . . 8
94 opeq2 3878 . . . . . . . . . . 11
9594breq1d 4114 . . . . . . . . . 10
9695mobidv 2244 . . . . . . . . 9
9796ralrn 5751 . . . . . . . 8
9811, 93, 973syl 18 . . . . . . 7
9998ralbidv 2639 . . . . . 6
10092, 99mpbird 223 . . . . 5
101 breq1 4107 . . . . . . 7
102101mobidv 2244 . . . . . 6
103102ralxp 4909 . . . . 5
104100, 103sylibr 203 . . . 4
105 ssralv 3313 . . . 4
10646, 104, 105sylc 56 . . 3
107 dffun7 5362 . . 3
10819, 106, 107sylanbrc 645 . 2
109 eqimss2 3307 . . . . . . . . . . . . . . 15
11017, 109syl 15 . . . . . . . . . . . . . 14
111 iunss 4024 . . . . . . . . . . . . . 14
112110, 111sylib 188 . . . . . . . . . . . . 13
113112r19.21bi 2717 . . . . . . . . . . . 12
114113adantrl 696 . . . . . . . . . . 11
115 dmss 4960 . . . . . . . . . . 11
116114, 115syl 15 . . . . . . . . . 10
11759, 116syl5eqssr 3299 . . . . . . . . 9
118 simprl 732 . . . . . . . . . 10
119 fvex 5622 . . . . . . . . . . 11
120119snid 3743 . . . . . . . . . 10
121 opelxpi 4803 . . . . . . . . . 10
122118, 120, 121sylancl 643 . . . . . . . . 9
123117, 122sseldd 3257 . . . . . . . 8
124123ralrimivva 2711 . . . . . . 7
125 opeq2 3878 . . . . . . . . . . 11
126125eleq1d 2424 . . . . . . . . . 10
127126ralrn 5751 . . . . . . . . 9
12811, 93, 1273syl 18 . . . . . . . 8
129128ralbidv 2639 . . . . . . 7
130124, 129mpbird 223 . . . . . 6
131 eleq1 2418 . . . . . . 7
132131ralxp 4909 . . . . . 6
133130, 132sylibr 203 . . . . 5
134 dfss3 3246 . . . . 5
135133, 134sylibr 203 . . . 4
13645, 135eqsstr3d 3289 . . 3
13742, 136eqssd 3272 . 2
138 df-fn 5340 . 2
139108, 137, 138sylanbrc 645 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wal 1540   wceq 1642   wcel 1710  wmo 2210   wne 2521  wral 2619  wrex 2620  cvv 2864   wss 3228  c0 3531  csn 3716  cop 3719  ciun 3986   class class class wbr 4104   cxp 4769   cdm 4771   crn 4772   wrel 4776   wfun 5331   wfn 5332  wf 5333  wfo 5335  cfv 5337  (class class class)co 5945   cmpt2 5947  cbs 13245  Scalarcsca 13308  cvsca 13309   s cimas 13506 This theorem is referenced by:  imasvscaval  13539  imasvscaf  13540 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-cnex 8883  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-mulcom 8891  ax-addass 8892  ax-mulass 8893  ax-distr 8894  ax-i2m1 8895  ax-1ne0 8896  ax-1rid 8897  ax-rnegex 8898  ax-rrecex 8899  ax-cnre 8900  ax-pre-lttri 8901  ax-pre-lttrn 8902  ax-pre-ltadd 8903  ax-pre-mulgt0 8904 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-int 3944  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-tr 4195  df-eprel 4387  df-id 4391  df-po 4396  df-so 4397  df-fr 4434  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-1st 6209  df-2nd 6210  df-riota 6391  df-recs 6475  df-rdg 6510  df-1o 6566  df-oadd 6570  df-er 6747  df-en 6952  df-dom 6953  df-sdom 6954  df-fin 6955  df-sup 7284  df-pnf 8959  df-mnf 8960  df-xr 8961  df-ltxr 8962  df-le 8963  df-sub 9129  df-neg 9130  df-nn 9837  df-2 9894  df-3 9895  df-4 9896  df-5 9897  df-6 9898  df-7 9899  df-8 9900  df-9 9901  df-10 9902  df-n0 10058  df-z 10117  df-dec 10217  df-uz 10323  df-fz 10875  df-struct 13247  df-ndx 13248  df-slot 13249  df-base 13250  df-plusg 13318  df-mulr 13319  df-sca 13321  df-vsca 13322  df-tset 13324  df-ple 13325  df-ds 13327  df-imas 13510
 Copyright terms: Public domain W3C validator